X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineStructuralRules.ml;h=20b0f21c9f307f0c8f9f05042f3f6aa4147f3f8d;hb=a6fc115fd7d4cfba94a43f001f4c27322d3db1a8;hp=7f4a89fb868bb0da871403047dc7dc4cd922d3a7;hpb=d651bf2e3d560e194fbe948dd950dd600a40eab6;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index 7f4a89fb8..20b0f21c9 100644
--- 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