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

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 080ba224d2cdfc223cc819910874d02de707ee54..98c13e80b8b742b775df418788b1eaa215fc17e1 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -23,7 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let search_theorems_in_context ~status:((proof,goal) as status) =
+let search_theorems_in_context status =
+  let (proof, goal) = status in
   let module C = Cic in
   let module R = CicReduction in
   let module S = CicSubstitution in
@@ -35,7 +36,7 @@ let search_theorems_in_context ~status:((proof,goal) as status) =
     | hd::tl ->
        let res =
          try 
-            Some (PrimitiveTactics.apply_tac ~status ~term:(C.Rel n)) 
+            Some (PrimitiveTactics.apply_tac status ~term:(C.Rel n)) 
          with 
            ProofEngineTypes.Fail _ -> None in
        (match res with
@@ -65,8 +66,8 @@ if level = 0 then
 else 
   (* choices is a list of pairs proof and goallist *)
   let choices  =
-    (search_theorems_in_context ~status:(proof,goal))@ 
-    (TacticChaser.searchTheorems mqi_handle ~status:(proof,goal)) 
+    (search_theorems_in_context (proof,goal))@ 
+    (TacticChaser.searchTheorems mqi_handle (proof,goal))
   in
   let rec try_choices = function
     [] -> raise NotApplicableTheorem
@@ -93,7 +94,7 @@ prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist));
             try_choices tl) in
  try_choices choices;;
 
-let auto_tac mqi_handle ~status:(proof,goal) = 
+let auto_tac mqi_handle (proof,goal) =
   prerr_endline "Entro in Auto";
   try 
     let proof = auto_tac mqi_handle depth proof goal in
@@ -109,7 +110,8 @@ prerr_endline "AUTO_TAC HA FINITO";
 chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
 funzione di callback che restituisce la (sola) hyp da applicare *)
 
-let assumption_tac ~status:((proof,goal) as status) =
+let assumption_tac status =
+  let (proof, goal) = status in
   let module C = Cic in
   let module R = CicReduction in
   let module S = CicSubstitution in
@@ -128,7 +130,7 @@ let assumption_tac ~status:((proof,goal) as status) =
            | _ -> find (n+1) tl
          )
       | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption")
-     in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
+     in PrimitiveTactics.apply_tac status ~term:(C.Rel (find 1 context))
 ;;
 
 (* ANCORA DA DEBUGGARE *)
@@ -141,8 +143,9 @@ contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
 
 let generalize_tac
  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
- terms ~status:((proof,goal) as status)
+ terms status
 =
+  let (proof, goal) = status in
   let module C = Cic in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
@@ -173,7 +176,7 @@ let generalize_tac
              ~where:ty)
          )))
       ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
-      ~status
+      status
 ;;