got rid of ~status label so that tactics can now be applied partially,

[helm.git] / helm / ocaml / tactics / proofEngineStructuralRules.ml

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index 7f4a89fb868bb0da871403047dc7dc4cd922d3a7..20b0f21c9f307f0c8f9f05042f3f6aa4147f3f8d 100644 (file)
--- a/helm/ocaml/tactics/proofEngineStructuralRules.ml
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml
@@ -25,7 +25,7 @@
 
 open ProofEngineTypes
 
-let clearbody ~hyp ~status:(proof, goal) =
+let clearbody ~hyp (proof, goal) =
  let module C = Cic in
   match hyp with
      None -> assert false
@@ -91,7 +91,7 @@ let clearbody ~hyp ~status:(proof, goal) =
         in
          (curi,metasenv',pbo,pty), [goal]
 
-let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
+let clear ~hyp:hyp_to_clear (proof, goal) =
  let module C = Cic in
   match hyp_to_clear with
      None -> assert false