diff options
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 0c0204081a..bf7e8b3487 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 |