added a (for the moment) dummy field _subst to ProofengineTypes.proof.

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

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index 79cf52e65fa7bfe791474ef02e08a52c6530e5c6..12041b2bc28a5354867ee6ca292d580bd48abd72 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,_subst,_,_, _ = 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,_subst,_,_, _ = 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,_subst, p,_, _ = proof in
     (* first of all we check if the goal has been already
        inspected *)
   assert (CicUtil.exists_meta goal metasenv);
@@ -148,12 +148,13 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
               (* if we just apply the subtitution, the type 
                  is irrelevant: we may use Implicit, since it will 
                  be dropped *)
-              CicMetaSubst.apply_subst 
-                [(goal,(ey, bo, Cic.Implicit None))] in
+                [(goal,(ey, bo, Cic.Implicit None))] 
+            in
+            let _ = assert false in
             let (proof,_) = 
               ProofEngineHelpers.subst_meta_and_metasenv_in_proof 
                 proof goal subst_in metasenv in
-              [(subst_in,(proof,[],sign))]
+              [(CicMetaSubst.apply_subst subst_in,(proof,[],sign))]
         | No d when (d >= depth) -> 
             (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *)
             [] (* the empty list means no choices, i.e. failure *)
@@ -228,7 +229,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, _subst, _,_, _ = proof in
       let goals'=
         List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
       in
@@ -244,7 +245,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,_subst,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 +285,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 _,_,_subst,p,_, _ = proof in
         debug_print (lazy (CicPp.ppterm p));
         debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)));
         (proof,[])