existential variables in goal supported

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

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index b6c3dc66a6625ec2e2ba92043e5108d6375f501d..34b69718f50413569c247ce90d7d443a44240017 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -465,18 +465,19 @@ let pp_proof names goalproof proof =
       ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
 ;;
 
-let build_goal_proof l initial ty =
-  let proof = 
+let build_goal_proof l initial ty se =
+  let se = List.map (fun i -> Cic.Meta (i,[])) se in 
+  let proof,se = 
    List.fold_left 
-   (fun  current_proof (pos,id,subst,pred) -> 
+   (fun (current_proof,se) (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
+        build_proof_step subst current_proof p pos l r pred,
+        List.map (fun x -> Subst.apply_subst subst x) se)
+   (initial,se) l
   in
-  proof 
-  (*canonical (contextualize_rewrites proof ty)*)
+  canonical (contextualize_rewrites proof ty), se
 ;;
 
 let refl_proof ty term = 
@@ -486,8 +487,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 +522,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