Build_proof_goal does not return the metasenv any more.

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

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 70f8f850feba7f7b29bbfd48dbafba002acbfd54..953635dbd8e65df346c11dbc45c0f683f4c3d42f 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -425,12 +425,12 @@ let build_proof_term_old ?(noproof=Cic.Implicit None) proof =
 
 let build_proof_term_new proof =
   let rec aux extra = function
-     | Exact term -> term, []
+     | Exact term -> term
      | Step (subst,(_, id1, (pos,id2), pred)) ->
          let p,m1,_,_ = proof_of_id id1 in
-         let p1,m2 = aux [] p in
+         let p1 = aux [] p in
          let p,m3,l,r = proof_of_id id2 in 
-         let p2,m4 = aux [] p in
+         let p2 = aux [] p in
          let p1 = apply_subst subst p1 in
          let p2 = apply_subst subst p2 in
          let l = apply_subst subst l in
@@ -451,23 +451,20 @@ let build_proof_term_new proof =
          in 
          (Cic.Appl [
            Cic.Const (eq_URI, []); 
-           ty; what; pred; p1; other; p2]), 
-         (apply_subst_metasenv subst (m1@m2@m3@m4))
+           ty; what; pred; p1; other; p2]) 
   in
    aux [] proof
-         
 
-let build_goal_proof l (refl,reflmenv) =
-  let proof, menv, subst = 
+let build_goal_proof l refl=
+  let proof, subst = 
    List.fold_left 
-   (fun  (current_proof,current_menv,current_subst) (pos,id,subst,pred) -> 
+   (fun  (current_proof,current_subst) (pos,id,subst,pred) -> 
       let p,m,l,r = proof_of_id id in
-      let p,m1 = build_proof_term_new p in
+      let p = build_proof_term_new p in
       let p = apply_subst subst p in
       let l = apply_subst subst l in
       let r = apply_subst subst r in
       let pred = apply_subst subst pred in
-      let newm = apply_subst_metasenv subst (m@m1) in
       let ty = (* Cic.Implicit None *) 
         match pred with
         | Cic.Lambda (_,ty,_) -> ty 
@@ -482,11 +479,10 @@ let build_goal_proof l (refl,reflmenv) =
           | Utils.Right ->  Utils.eq_ind_URI () 
       in
         ((Cic.Appl [Cic.Const (eq_URI, []);
-          ty; what; pred; current_proof; other; p]), 
-         current_menv @ newm, subst @ current_subst))
-   (refl,reflmenv,[]) l
+          ty; what; pred; current_proof; other; p]), subst @ current_subst))
+   (refl,[]) l
   in
-  proof, menv
+  proof
 ;;
 
 let refl_proof ty term =