X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=7d981cf316f92611101631e01dceec5e522e7557;hb=347a92a83c3fa154c850d94b1a211fbb8334d4f1;hp=8f696d6f3e330b960c0d3782c62f2d3720f46ece;hpb=abb7b4623d6c2eb93f289c44fe46f45faa7e3374;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 8f696d6f3..7d981cf31 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -367,6 +367,7 @@ let rec find_all_matches ?(unif_fun=Founif.unification)
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
+  (* prerr_endline ("matching " ^  CicPp.ppterm term); *)
   let cmp = !Utils.compare_terms in
   let check = match termty with C.Implicit None -> false | _ -> true in
   function
@@ -537,7 +538,7 @@ let subsumption_aux_all use_unification env table target =
           let what' = Subst.apply_subst subst what in
           let other' = Subst.apply_subst subst other in
           let subst', menv', ug' =
-            unif_fun metasenv m context what' other' ugraph
+            unif_fun [] menv context what' other' ugraph
           in
           (match Subst.merge_subst_if_possible subst subst' with
           | None -> ok_all what leftorright tl
@@ -555,7 +556,7 @@ let subsumption_all x y z =
 ;;
 
 let unification_all x y z = 
-  subsumption_aux_all true x y z
+  prerr_endline "unification_all"; subsumption_aux_all true x y z
 ;;
 
 let rec demodulation_aux bag ?from ?(typecheck=false) 
@@ -752,7 +753,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
   in
 
   let res = 
-    demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left 
+    demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left 
   in
   if Utils.debug_res then check_res res "demod result";
   let newmeta, newtarget = 
@@ -904,6 +905,7 @@ let rec betaexpand_term
          CicTypeChecker.type_of_aux' metasenv context term ugraph 
       in
       let candidates = get_candidates Unification table term in
+      (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
       let r = 
         if subterms_only then 
           [] 
@@ -1074,10 +1076,9 @@ let build_newg bag context goal rule expansion =
       Utils.guarded_simpl context 
         (apply_subst subst (CicSubstitution.subst other t)) 
     in
-    let bo' = apply_subst subst t in
-    let ty = apply_subst subst ty in 
-    let name = Cic.Name "x" in 
-    let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+    let name = Cic.Name "x" in     
+    let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in 
+    let newgoalproofstep = (rule,pos,id,subst,pred) in
     bo, (newgoalproofstep::goalproof)
   in
   let newmetasenv = (* Founif.filter subst *) menv in
@@ -1149,10 +1150,9 @@ let build_newgoal bag context goal posu rule expansion =
       Utils.guarded_simpl context 
         (apply_subst subst (CicSubstitution.subst other t)) 
     in
-    let bo' = apply_subst subst t in
-    let ty = apply_subst subst ty in 
     let name = Cic.Name "x" in 
-    let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+    let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in 
+    let newgoalproofstep = (rule,pos,id,subst,pred) in
     bo, (newgoalproofstep::goalproof)
   in
   let newmetasenv = (* Founif.filter subst *) menv in
@@ -1183,7 +1183,7 @@ let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
       end
     else
         match c with 
-        | Utils.Gt -> (* prerr_endline "GT"; *) 
+        | Utils.Gt -> 
             let big,small,possmall = l,r,Utils.Right in
             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
             List.map