commented out a line to help paramodulation.

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

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index b6c3dc66a6625ec2e2ba92043e5108d6375f501d..521c7635c09f850c0363cb1c2cccffe491f43f69 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -465,18 +465,23 @@ let pp_proof names goalproof proof =
       ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
 ;;
 
-let build_goal_proof l initial ty =
-  let proof = 
-   List.fold_left 
-   (fun  current_proof (pos,id,subst,pred) -> 
-      let p,l,r = proof_of_id id in
-      let p = build_proof_term p in
-      let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
-        build_proof_step subst current_proof p pos l r pred)
-   initial l
+let build_goal_proof l initial ty se =
+  let se = List.map (fun i -> Cic.Meta (i,[])) se in 
+  let proof,se = 
+    let rec aux se current_proof = function
+      | [] -> current_proof,se
+      | (pos,id,subst,pred)::tl ->
+           let p,l,r = proof_of_id id in
+           let p = build_proof_term p in
+           let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
+           let proof = build_proof_step subst current_proof p pos l r pred in
+           let proof,se = aux se proof tl in
+           Subst.apply_subst subst proof,
+           List.map (fun x -> Subst.apply_subst subst x) se
+    in
+    aux se initial l
   in
-  proof 
-  (*canonical (contextualize_rewrites proof ty)*)
+  canonical (contextualize_rewrites proof ty), se
 ;;
 
 let refl_proof ty term = 
@@ -486,8 +491,9 @@ let refl_proof ty term =
        ty; term]
 ;;
 
-let metas_of_proof p = 
-  Utils.metas_of_term (build_proof_term p)
+let metas_of_proof p =
+  let p = build_proof_term p in
+  Utils.metas_of_term p
 ;;
 
 let relocate newmeta menv =
@@ -520,7 +526,7 @@ let fix_metas newmeta eq =
   let fix_proof = function
     | Exact p -> Exact (Subst.apply_subst subst p)
     | Step (s,(r,id1,(pos,id2),pred)) -> 
-        Step (Subst.concat_substs s subst,(r,id1,(pos,id2), pred))
+        Step (Subst.concat s subst,(r,id1,(pos,id2), pred))
   in
   let p = fix_proof p in
   let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in