Removed the context from the metasenv to avoid trivial typing errors (lists

[helm.git] / helm / software / components / tactics / paramodulation / indexing.ml

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 77a377a88bfd67d8987bfdd4adfec094961ca468..7d981cf316f92611101631e01dceec5e522e7557 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -905,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 
           [] 
@@ -1075,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
@@ -1150,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
@@ -1184,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