simplify has a brand new semantics!

[helm.git] / components / tactics / autoTactic.ml

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index e8d034a3298a9630fa0c8b1efe693579a1045ed2..79cf52e65fa7bfe791474ef02e08a52c6530e5c6 100644 (file)
--- a/components/tactics/autoTactic.ml
+++ b/components/tactics/autoTactic.ml
@@ -56,7 +56,7 @@ let search_theorems_in_context status =
   let module S = CicSubstitution in
   let module PET = ProofEngineTypes in 
   let module PT = PrimitiveTactics in 
-  let _,metasenv,_,_ = proof in
+  let _,metasenv,_,_, _ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
   let rec find n = function 
     | [] -> []
@@ -89,7 +89,7 @@ let search_theorems_in_context status =
 
 
 let compare_goals proof goal1 goal2 =
-  let _,metasenv,_,_ = proof in
+  let _,metasenv,_,_, _ = proof in
   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
   let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1 
@@ -129,7 +129,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
   if List.mem ty already_seen_goals then [] else
   let already_seen_goals = ty::already_seen_goals in
   let facts = (depth = 1) in  
-  let _,metasenv,p,_ = proof in
+  let _,metasenv,p,_, _ = proof in
     (* first of all we check if the goal has been already
        inspected *)
   assert (CicUtil.exists_meta goal metasenv);
@@ -228,7 +228,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
 and auto_new dbd width already_seen_goals universe = function
   | [] -> []
   | (subst,(proof, goals, sign))::tl ->
-      let _,metasenv,_,_ = proof in
+      let _,metasenv,_,_, _ = proof in
       let goals'=
         List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
       in
@@ -244,7 +244,7 @@ and auto_new_aux dbd width already_seen_goals universe = function
       (List.length goals) > width -> 
       auto_new dbd width already_seen_goals universe tl 
   | (subst,(proof, (goal,depth)::gtl, sign))::tl -> 
-      let _,metasenv,p,_ = proof in
+      let _,metasenv,p,_, _ = proof in
       let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
       match (auto_single dbd proof goal ey ty depth
         (width - (List.length gtl)) sign already_seen_goals) universe
@@ -284,7 +284,7 @@ let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
     | (_,(proof,[],_))::_ ->
         let t2 = Unix.gettimeofday () in
         debug_print (lazy "AUTO_TAC HA FINITO");
-        let _,_,p,_ = proof in
+        let _,_,p,_, _ = proof in
         debug_print (lazy (CicPp.ppterm p));
         debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)));
         (proof,[])