diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-11-09 19:44:17 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-11-09 19:44:17 +0100 |
| commit | ce80fa3cb3e6d8809bb3ee015bff39c67c0aed16 (patch) | |
| tree | be80159f44855799c885174910de3931fdde07b2 /tactics | |
| parent | 91c2a866e7827c0ede0539cb49f924b68db569a9 (diff) | |
new: Optimize Proof, Optimize Heap
- drops all Defined entries from the evar map (applying the subst to the
initial evar and the undefined evars types).
- call Gc.compact
Now the question is: where should these two commands be documented?
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 0c0204081..bf7e8b348 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -998,3 +998,11 @@ END VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY | [ "Print" "Equivalent" "Keys" ] -> [ msg_info (Keys.pr_keys Printer.pr_global) ] END + + +VERNAC COMMAND EXTEND OptimizeProof +| [ "Optimize" "Proof" ] => [ Vernac_classifier.classify_as_proofstep ] -> + [ Proof_global.compact_the_proof () ] +| [ "Optimize" "Heap" ] => [ Vernac_classifier.classify_as_proofstep ] -> + [ Gc.compact () ] +END |