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

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

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index fe593a4f81c365b0eaa281880fd0ee6791f21ac8..5851b1467e9e583863c9258d658fedc2d58cb52d 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -40,7 +40,7 @@ module U = MQGUtil
 module G = MQueryGenerator
 
   (* search arguments on which Apply tactic doesn't fail *)
-let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() ~status =
+let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
  let ((_, metasenv, _, _), metano) = status in
  let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
   let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
@@ -80,7 +80,7 @@ match list_of_must with
               (PrimitiveTactics.apply_tac
                ~term:(MQueryMisc.term_of_cic_textual_parser_uri
                 (MQueryMisc.cic_textual_parser_uri_of_string uri))
-               ~status);
+               status);
              true
             with ProofEngineTypes.Fail _ -> false)
            then
@@ -111,7 +111,7 @@ match list_of_must with
 
 
 (*matchConclusion modificata per evitare una doppia apply*)
-let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() ~status =
+let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
  let ((_, metasenv, _, _), metano) = status in
  let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
   let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
@@ -151,7 +151,7 @@ match list_of_must with
               ((PrimitiveTactics.apply_tac
                ~term:(MQueryMisc.term_of_cic_textual_parser_uri
                 (MQueryMisc.cic_textual_parser_uri_of_string uri))
-               ~status)::tl')
+               status)::tl')
             with ProofEngineTypes.Fail _ -> tl'
      in    
      prerr_endline (string_of_int (List.length uris));
@@ -192,14 +192,14 @@ let position n =
 (*function taking a status and returning a new status after having searching a theorem to apply ,theorem which *)
 (*generate the less number of subgoals*)
 
-let  searchTheorem ~status:(proof,goal) =
+let  searchTheorem (proof,goal) =
   let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
   in
     let mqi_handle = MQIC.init mqi_flags prerr_string
 in
   let uris' =
     matchConclusion
-      mqi_handle ~choose_must() ~status:(proof, goal)
+      mqi_handle ~choose_must() (proof, goal)
   in
   let list_of_termin =
     List.map
@@ -212,7 +212,7 @@ in
   let list_proofgoal =
     List.map
     (function term ->
-      PrimitiveTactics.apply_tac ~term ~status:(proof,goal))
+      PrimitiveTactics.apply_tac ~term (proof,goal))
     list_of_termin
   in
   let (list_of_subgoal: int  list list) =
@@ -234,15 +234,15 @@ in
 
   (* modifico la str in modo che sia accettata da apply*)
   in*)
-  PrimitiveTactics.apply_tac ~term:uri' ~status:(proof,goal)
+  PrimitiveTactics.apply_tac ~term:uri' (proof,goal)
 ;;
 *)
 
 
-let  searchTheorems mqi_handle ~status:(proof,goal) =
+let  searchTheorems mqi_handle (proof,goal) =
 (*prerr_endline "1";*)
   let uris' =
-    matchConclusion2 mqi_handle ~choose_must() ~status:(proof, goal) in
+    matchConclusion2 mqi_handle ~choose_must() (proof, goal) in
 prerr_endline (string_of_int (List.length uris'));
 (*prerr_endline "2";*)
 (*  let list_of_termin =
@@ -255,7 +255,7 @@ prerr_endline "3";
   let list_proofgoal =
     List.map
       (function term ->
-         PrimitiveTactics.apply_tac ~term ~status:(proof,goal)) list_of_termin in*)
+         PrimitiveTactics.apply_tac ~term (proof,goal)) list_of_termin in*)
 (*prerr_endline "4";*)
 let res =
   List.sort