X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineStructuralRules.ml;h=b1e23751f413afb1b7280bc56a2b1879ca943f73;hb=115915f23df4f56832d68b2f6b5b80c5afe019fc;hp=4677a33ac8221a1080d7d0f6953e9fe2b8a822ba;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/tactics/proofEngineStructuralRules.ml b/components/tactics/proofEngineStructuralRules.ml
index 4677a33ac..b1e23751f 100644
--- a/components/tactics/proofEngineStructuralRules.ml
+++ b/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 *)