From c1960c794b5c8444925df67663bd70d35c67dc36 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 3 Jan 2018 14:42:52 -0500
Subject: add optimize_heap tactic for #6488

---
 plugins/ltac/extratactics.ml4 | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'plugins')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 982fc7cc3c..b222e1387a 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -1117,3 +1117,12 @@ VERNAC COMMAND EXTEND OptimizeProof
 | [ "Optimize" "Heap" ] => [ Vernac_classifier.classify_as_proofstep ] ->
   [ Gc.compact () ]
 END
+
+(** tactic analogous to "OPTIMIZE HEAP" *)
+
+let tclOPTIMIZE_HEAP =
+  Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ()))
+
+TACTIC EXTEND optimize_heap
+| [ "optimize_heap" ] -> [ tclOPTIMIZE_HEAP ]
+END
-- 
cgit v1.2.3