Build_proof_goal does not return the metasenv any more.

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 70f8f850feba7f7b29bbfd48dbafba002acbfd54..953635dbd8e65df346c11dbc45c0f683f4c3d42f 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/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 = 

diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli
index 9ef8d2197661b5877e74610441512f4d8571897e..4d48f22aade7a4aa888b99d924963731e918f3ce 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.mli
+++ b/helm/software/components/tactics/paramodulation/equality.mli
@@ -80,10 +80,9 @@ val string_of_equality : ?env:Utils.environment -> equality -> string
 val string_of_proof_old : ?names:(Cic.name option)list -> old_proof -> string
 val string_of_proof_new : 
   ?names:(Cic.name option)list -> new_proof -> goal_proof -> string
-val build_proof_term_new: new_proof -> Cic.term * Cic.metasenv
+val build_proof_term_new: new_proof -> Cic.term 
 val build_proof_term_old: ?noproof:Cic.term -> old_proof -> Cic.term
-val build_goal_proof: 
-  goal_proof -> (Cic.term * Cic.metasenv) -> Cic.term * Cic.metasenv
+val build_goal_proof: goal_proof -> Cic.term -> Cic.term
 val refl_proof: Cic.term -> Cic.term -> Cic.term 
 (** ensures that metavariables in equality are unique *)
 val fix_metas: int -> equality -> int * equality

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 1f9f5d5762e3c5b4072e343a5d0458ad7a238d7b..f3314bfa022d461b81c63de3f9921db6d6a8fa04 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -602,7 +602,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
   let order = !Utils.compare_terms left right in
   let stat = (eq_ty, left, right, order) in 
   let w = Utils.compute_equality_weight stat in
-  let target = Equality.mk_equality (w, proof, stat, metas) in
+  (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
   if Utils.debug_metas then 
     ignore(check_target context target "demod equalities input");
   let metasenv' = (* metasenv @ *) metas in
@@ -745,6 +745,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
     match res with
     | Some t ->
         let newmeta, newtarget = build_newtarget true t in
+         assert (not (Equality.meta_convertibility_eq target newtarget));
           if (Equality.is_weak_identity newtarget) ||
             (Equality.meta_convertibility_eq target newtarget) then
               newmeta, newtarget

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index d5da5485f72526bc4ded022d3953dc7acd5ff50e..4423661b00b118073a45e4d0d071bfec56c8921a 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -857,7 +857,7 @@ let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table =
                    repl proof
                in
                let newcicp,np,subst,cicmenv = 
-                 cicproof,np, subst, (m @ menv) 
+                 cicproof,np, subst, Equality.apply_subst_metasenv subst (m @ menv) 
                in
                  Some 
                   ((newcicp,np,subst,cicmenv),
@@ -1492,14 +1492,10 @@ let saturate
       let cic_proof = Equality.build_proof_term_old proof in
      
       (* generation of the new proof *)
-      let cic_proof_new,cic_proof_new_menv = 
+      let cic_proof_new = 
         Equality.build_goal_proof 
           goalproof (Equality.build_proof_term_new newproof) 
       in
-      let newproof_menv = 
-        Equality.apply_subst_metasenv subsumption_subst 
-          (newproof_menv @ cic_proof_new_menv)
-      in
       let cic_proof_new = 
         Equality.apply_subst subsumption_subst cic_proof_new 
       in

diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index 7d55e75899940b582d74adc5bf3ae6665c257e89..67127e640e10e50c33928aa198ec4d6a570b7efd 100644 (file)
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Apr  5 15:04:24 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Apr 12 11:46:23 CEST 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val assumption : ProofEngineTypes.tactic