X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Finference.ml;h=272a8100337c082485a6935fe270d5d3a2c8827f;hb=97d5c628470f472501ee41a5cc2e045ca89bfbf0;hp=f088d54543aa265f6550e53bf0552f886c409e8f;hpb=ba2372bd35aec412f5a7b61e5431236505567c43;p=helm.git

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index f088d5454..272a81003 100644
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -30,7 +30,7 @@ open Printf;;
 
 let check_disjoint_invariant subst metasenv msg =
   if (List.exists 
-        (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
+        (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
   then 
     begin 
       prerr_endline ("not disjoint: " ^ msg);
@@ -65,7 +65,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
   let module C = Cic in
   let module M = CicMetaSubst in
   let module U = CicUnification in
-  let lookup = Equality.lookup_subst in
+  let lookup = Subst.lookup_subst in
   let rec occurs_check subst what where =
     match where with
     | t when what = t -> true
@@ -99,8 +99,8 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
     | C.Meta (i, l), t -> (
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
-          assert (not (Equality.is_in_subst i subst));
-          let subst = Equality.buildsubst i context t ty subst in
+          assert (not (Subst.is_in_subst i subst));
+          let subst = Subst.buildsubst i context t ty subst in
           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
           subst, menv
         with CicUtil.Meta_not_found m ->
@@ -126,8 +126,8 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
     | _, _ ->
         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
   in
-  let subst, menv = unif Equality.empty_subst metasenv t1 t2 in
-  let menv = Equality.filter subst menv in
+  let subst, menv = unif Subst.empty_subst metasenv t1 t2 in
+  let menv = Subst.filter subst menv in
   subst, menv, ugraph
 ;;
 
@@ -234,10 +234,7 @@ let find_equalities context proof =
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
-                    let proof_old = 
-                      Equality.BasicProof (Equality.empty_subst,p) in
-                    let proof_new = Equality.Exact p in
-                    let proof = proof_new , proof_old in
+                    let proof = Equality.Exact p in
                     let e = Equality.mk_equality (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
@@ -251,9 +248,7 @@ let find_equalities context proof =
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
               let p = C.Rel index in
-              let proof_old = Equality.BasicProof (Equality.empty_subst,p) in
-              let proof_new = Equality.Exact p in
-              let proof = proof_new, proof_old in
+              let proof = Equality.Exact p in
               let e = Equality.mk_equality (w, proof,stat,[]) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
@@ -391,10 +386,7 @@ let find_library_equalities dbd context status maxmeta =
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
-                    let proof_old = 
-                      Equality.BasicProof (Equality.empty_subst,p) in
-                    let proof_new = Equality.Exact p in
-                    let proof = proof_new, proof_old in
+                    let proof = Equality.Exact p in
                     let e = Equality.mk_equality (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
@@ -404,9 +396,7 @@ let find_library_equalities dbd context status maxmeta =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let old_proof = Equality.BasicProof (Equality.empty_subst,term) in
-              let new_proof = Equality.Exact term in 
-              let proof = new_proof, old_proof in
+              let proof = Equality.Exact term in 
               let e = Equality.mk_equality (w, proof, stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta