From ce80fa3cb3e6d8809bb3ee015bff39c67c0aed16 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 9 Nov 2014 19:44:17 +0100 Subject: 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? --- tactics/extratactics.ml4 | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'tactics') 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 -- cgit v1.2.3