X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=98c13e80b8b742b775df418788b1eaa215fc17e1;hb=a6fc115fd7d4cfba94a43f001f4c27322d3db1a8;hp=080ba224d2cdfc223cc819910874d02de707ee54;hpb=d651bf2e3d560e194fbe948dd950dd600a40eab6;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 080ba224d..98c13e80b 100644
--- 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
 ;;