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 3b91f5f91c1cf67ae6c87c46cf72a451c7ab4eb8..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 
           [] 
@@ -1077,7 +1078,7 @@ let build_newg bag context goal rule expansion =
     in
     let name = Cic.Name "x" in     
     let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in 
-    let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+    let newgoalproofstep = (rule,pos,id,subst,pred) in
     bo, (newgoalproofstep::goalproof)
   in
   let newmetasenv = (* Founif.filter subst *) menv in
@@ -1176,15 +1177,13 @@ let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
       prerr_endline (string_of_int (List.length expansionsl));
       prerr_endline (string_of_int (List.length expansionsr));
       *)
-      if expansionsl <> [] then prerr_endline "expansionl";
-      if expansionsr <> [] then prerr_endline "expansionr";
       List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
       @
       List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
       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