Subsumption_subst must be applied to the initial proof before passing

[helm.git] / components / tactics / paramodulation / equality.ml

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 2561ea56f5a587549fdc89f6fb55fc56ecc8aece..3979c052985f76f542a68ad1c409ef8cf4274a44 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -422,7 +422,14 @@ let contextualize_rewrites t ty =
   let eq,ty,l,r = open_eq ty in
   contextualize eq ty l r t
 ;;
-  
+
+let add_subst subst =
+  function
+    | Exact t -> Exact (Subst.apply_subst subst t)
+    | Step (s,(rule, id1, (pos,id2), pred)) -> 
+       Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
+;;
+       
 let build_proof_step ?(sym=false) lift subst p1 p2 pos l r pred =
   let p1 = Subst.apply_subst_lift lift subst p1 in
   let p2 = Subst.apply_subst_lift lift subst p2 in
@@ -722,8 +729,9 @@ let build_goal_proof l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-  canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), 
-   se
+    (proof,se)
+  (* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+   se *)
 ;;
 
 let refl_proof ty term = 
@@ -756,6 +764,7 @@ let relocate newmeta menv to_be_relocated =
 let fix_metas newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
   let to_be_relocated = 
+(* List.map (fun i ,_,_ -> i) menv *)
     HExtlib.list_uniq 
       (List.sort Pervasives.compare 
          (Utils.metas_of_term left @ Utils.metas_of_term right))