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

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 232911450400654bed1c31db192f100e4303f0f1..0e9f72b0f96b73d65ea5644a85dbdceda93913d6 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -24,7 +24,7 @@
  *)
 
 
-let rewrite_tac ~term:equality ~status:(proof,goal) =
+let rewrite_tac ~term:equality (proof,goal) =
  let module C = Cic in
  let module U = UriManager in
   let curi,metasenv,pbo,pty = proof in
@@ -63,23 +63,23 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
       PrimitiveTactics.exact_tac
        ~term:(C.Appl
          [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
-        ~status:((curi,metasenv',pbo,pty),goal)
+          ((curi,metasenv',pbo,pty),goal)
      in
       assert (List.length goals = 0) ;
       (proof',[fresh_meta])
 ;;
 
 
-let rewrite_simpl_tac ~term ~status =
+let rewrite_simpl_tac ~term status =
  Tacticals.then_ 
   ~start:(rewrite_tac ~term)
   ~continuation:
    (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
-  ~status
+  status
 ;;
 
 
-let rewrite_back_tac ~term:equality ~status:(proof,goal) =
+let rewrite_back_tac ~term:equality (proof,goal) =
  let module C = Cic in
  let module U = UriManager in
   let curi,metasenv,pbo,pty = proof in
@@ -118,7 +118,7 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) =
       PrimitiveTactics.exact_tac
        ~term:(C.Appl
          [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
-        ~status:((curi,metasenv',pbo,pty),goal)
+        ((curi,metasenv',pbo,pty),goal)
      in
       assert (List.length goals = 0) ;
       (proof',[fresh_meta])
@@ -126,16 +126,17 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) =
 ;;
 
 
-let rewrite_back_simpl_tac ~term ~status =
+let rewrite_back_simpl_tac ~term status =
  Tacticals.then_ 
   ~start:(rewrite_back_tac ~term)
   ~continuation:
    (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
-  ~status
+  status
 ;;
 
 
-let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
+let replace_tac ~what ~with_what status =
+  let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
   let module P = PrimitiveTactics in
@@ -161,7 +162,7 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
                  ProofEngineStructuralRules.clear
                   ~hyp:(List.hd context)) ;
             T.id_tac]
-          ~status
+          status
        else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
        with (Failure "hd") -> raise (ProofEngineTypes.Fail "Replace: empty context")
 ;;
@@ -174,7 +175,7 @@ let reflexivity_tac =
 ;;
 
 
-let symmetry_tac ~status:(proof, goal) =
+let symmetry_tac (proof, goal) =
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
@@ -182,14 +183,15 @@ let symmetry_tac ~status:(proof, goal) =
     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri HelmLibraryObjects.Logic.eq_URI) ->
-         PrimitiveTactics.apply_tac ~status:(proof,goal)
+         PrimitiveTactics.apply_tac (proof,goal)
           ~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []))
 
       | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
 ;;
 
 
-let transitivity_tac ~term ~status:((proof, goal) as status) =
+let transitivity_tac ~term status =
+  let (proof, goal) = status in
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
@@ -203,7 +205,7 @@ let transitivity_tac ~term ~status:((proof, goal) as status) =
             ~term: (C.Const (HelmLibraryObjects.Logic.trans_eq_URI, [])))
           ~continuations:
             [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac]
-          ~status
+          status
 
       | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
 ;;