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

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 5909075d82f7aaf395d41ff5be5a2b2e4f887cc0..30d08c9bd76f7cdb52758a816c2dd653f422ef68 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -250,7 +250,7 @@ let
     new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
 ;;
 
-let apply_tac ~term ~status:(proof, goal) =
+let apply_tac ~term (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
  let module R = CicReduction in
@@ -328,16 +328,16 @@ let apply_tac ~term ~status:(proof, goal) =
 
   (* TODO per implementare i tatticali e' necessario che tutte le tattiche
   sollevino _solamente_ Fail *)
-let apply_tac ~term ~status =
+let apply_tac ~term status =
   try
-    apply_tac ~term ~status
+    apply_tac ~term status
       (* TODO cacciare anche altre eccezioni? *)
   with CicUnification.UnificationFailure _ as e ->
     raise (Fail (Printexc.to_string e))
 
 let intros_tac
  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()
- ~status:(proof, goal)
+ (proof, goal)
 =
  let module C = Cic in
  let module R = CicReduction in
@@ -354,7 +354,7 @@ let intros_tac
 
 let cut_tac
  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
- term ~status:(proof, goal)
+ term (proof, goal)
 =
  let module C = Cic in
   let curi,metasenv,pbo,pty = proof in
@@ -386,7 +386,7 @@ let cut_tac
 
 let letin_tac
  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
- term ~status:(proof, goal)
+ term (proof, goal)
 =
  let module C = Cic in
   let curi,metasenv,pbo,pty = proof in
@@ -410,7 +410,7 @@ let letin_tac
        (newproof, [newmeta])
 
   (** functional part of the "exact" tactic *)
-let exact_tac ~term ~status:(proof, goal) =
+let exact_tac ~term (proof, goal) =
  (* Assumption: the term bo must be closed in the current context *)
  let (_,metasenv,_,_) = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
@@ -428,7 +428,7 @@ let exact_tac ~term ~status:(proof, goal) =
 
 (* not really "primitive" tactics .... *)
 
-let elim_tac ~term ~status:(proof, goal) =
+let elim_tac ~term (proof, goal) =
  let module T = CicTypeChecker in
  let module U = UriManager in
  let module R = CicReduction in
@@ -571,7 +571,7 @@ exception NotConvertible
 (*CSC: while [what] can have a richer context (because of binders)           *)
 (*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
 (*CSC: Is that evident? Is that right? Or should it be changed?              *)
-let change_tac ~what ~with_what ~status:(proof, goal) =
+let change_tac ~what ~with_what (proof, goal) =
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   (* are_convertible works only on well-typed terms *)