CHANGES:
Big improvements in Lambdapi and Coq file generation time, and Coq checking time.
Added
- hol2dk can now generate term abbreviations and proofs in several files
in parallel:- The option --max-size-abbrev allows to fix the maximum size for term abbreviations files.
- The option --max-size-proof allows to fix the maximum size for proof files.
- optimization of lp file dependencies in generated lp files.
- generation of Makefile lpo dependencies at the same time as lp files.
- Makefile: lpo and vo dependencies are recomputed automatically.
Changed
- FILES_WITH_SHARING renamed into BIG_FILES and not added by add-links anymore
- command dump[-simp]-use renamed into dump[-simp]-before-hol
- for each theorem, two files are generated: one with the proof, and one declaring the theorem as an axiom