Implemented:

[helm.git] / helm / software / components / tactics / proofEngineStructuralRules.ml

diff --git a/helm/software/components/tactics/proofEngineStructuralRules.ml b/helm/software/components/tactics/proofEngineStructuralRules.ml
index 4677a33ac8221a1080d7d0f6953e9fe2b8a822ba..b1e23751f413afb1b7280bc56a2b1879ca943f73 100644 (file)
--- a/helm/software/components/tactics/proofEngineStructuralRules.ml
+++ b/helm/software/components/tactics/proofEngineStructuralRules.ml
@@ -97,8 +97,8 @@ let clearbody ~hyp =
  in
   mk_tactic (clearbody ~hyp)
 
-let clear ~hyp =
- let clear ~hyp (proof, goal) =
+let clear_one ~hyp =
+ let clear_one ~hyp (proof, goal) =
   let module C = Cic in
    let curi,metasenv,pbo,pty = proof in
     let metano,context,ty =
@@ -154,7 +154,19 @@ let clear ~hyp =
      in
       (curi,metasenv',pbo,pty), [goal]
  in
-  mk_tactic (clear ~hyp)
+  mk_tactic (clear_one ~hyp)
+
+let clear ~hyps =
+   let clear hyps status =
+      let aux status hyp = 
+         match apply_tactic (clear_one ~hyp) status with
+           | proof, [g] -> proof, g
+           | _          -> raise (Fail (lazy "clear: internal error"))
+      in
+      let proof, g = List.fold_left aux status hyps in
+      proof, [g]
+   in
+   mk_tactic (clear hyps)
 
 (* Warning: this tactic has no effect on the proof term.
    It just changes the name of an hypothesis in the current sequent *)