From 73cdb000ec07ec484557839c4b94fcf779df2f06 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 13 May 2016 00:16:09 +0200
Subject: Put the "clear" tactic into the monad.

---
 plugins/decl_mode/decl_proof_instr.ml | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 090b293f5c..4f22703130 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -34,6 +34,22 @@ open Context.Named.Declaration
 
 (* Strictness option *)
 
+let clear ids { it = goal; sigma } =
+  let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
+  let env = Goal.V82.env sigma goal in
+  let sign = Goal.V82.hyps sigma goal in
+  let cl = Goal.V82.concl sigma goal in
+  let evdref = ref (Evd.clear_metas sigma) in
+  let (hyps, concl) =
+    try Evarutil.clear_hyps_in_evi env evdref sign cl ids
+    with Evarutil.ClearDependencyError (id, _) ->
+      errorlabstrm "" (str "Cannot clear " ++ pr_id id)
+  in
+  let sigma = !evdref in
+  let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
+  let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
+  { it = [gl]; sigma }
+
 let get_its_info gls = get_info gls.sigma gls.it
 
 let get_strictness,set_strictness =
-- 
cgit v1.2.3