X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=105b708e92d47d21c4b812d58876f405fe9347bd;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=003fb958430cf9597bc46909e06867c33db6018a;hpb=b6bec181b81b3cbc56ec8914dcd7e6a029c7d84f;p=helm.git

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 003fb9584..105b708e9 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -378,8 +378,7 @@ let unification_simple metasenv context t1 t2 ugraph =
         unif subst menv t s
     | C.Meta _, t when occurs_check subst s t ->
         raise
-          (U.UnificationFailure
-             (U.failure_msg_of_string "Inference.unification.unif"))
+          (U.UnificationFailure (lazy "Inference.unification.unif"))
     | C.Meta (i, l), t -> (
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
@@ -400,20 +399,17 @@ let unification_simple metasenv context t1 t2 ugraph =
       )
     | _, C.Meta _ -> unif subst menv t s
     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
-        raise (U.UnificationFailure
-                 (U.failure_msg_of_string "Inference.unification.unif"))
+        raise (U.UnificationFailure (lazy "Inference.unification.unif"))
     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
         try
           List.fold_left2
             (fun (subst', menv) s t -> unif subst' menv s t)
             (subst, menv) tls tlt
         with Invalid_argument _ ->
-          raise (U.UnificationFailure
-                   (U.failure_msg_of_string "Inference.unification.unif"))
+          raise (U.UnificationFailure (lazy "Inference.unification.unif"))
       )
     | _, _ ->
-        raise (U.UnificationFailure
-                 (U.failure_msg_of_string "Inference.unification.unif"))
+        raise (U.UnificationFailure (lazy "Inference.unification.unif"))
   in
   let subst, menv = unif [] metasenv t1 t2 in
   let menv =
@@ -453,7 +449,7 @@ let unification metasenv context t1 t2 ugraph =
 ;;
 
 
-(* let unification = CicUnification.fo_unif;; *)
+let unification = CicUnification.fo_unif;;
 
 exception MatchingFailure;;
 
@@ -594,6 +590,7 @@ let find_equalities context proof =
 ;;
 
 
+(*
 let equations_blacklist =
   List.fold_left
     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
@@ -626,6 +623,9 @@ let equations_blacklist =
       "cic:/matita/logic/equality/eq_rect.con";
     ]
 ;;
+*)
+let equations_blacklist = UriManager.UriSet.empty;;
+
 
 let find_library_equalities dbd context status maxmeta = 
   let module C = Cic in
@@ -728,13 +728,13 @@ let find_library_equalities dbd context status maxmeta =
   let uriset, eqlist = 
     (List.fold_left
        (fun (s, l) (u, e) ->
-          if List.exists (meta_convertibility_eq e) l then (
+          if List.exists (meta_convertibility_eq e) (List.map snd l) then (
             debug_print
               (lazy
                  (Printf.sprintf "NO!! %s already there!"
                     (string_of_equality e)));
             (UriManager.UriSet.add u s, l)
-          ) else (UriManager.UriSet.add u s, e::l))
+          ) else (UriManager.UriSet.add u s, (u, e)::l))
        (UriManager.UriSet.empty, []) found)
   in
   uriset, eqlist, maxm
@@ -915,9 +915,10 @@ let equality_of_term proof term =
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 
 
-let is_identity ((_, context, ugraph) as env) = function
-  | ((_, _, (ty, left, right, _), _, _) as equality) ->
+let is_identity ((metasenv, context, ugraph) as env) = function
+  | ((_, _, (ty, left, right, _), menv, _) as equality) ->
       (left = right ||
-          (meta_convertibility left right) ||
-          (fst (CicReduction.are_convertible context left right ugraph)))
+          (* (meta_convertibility left right) || *)
+          (fst (CicReduction.are_convertible 
+		  ~metasenv:(metasenv @ menv) context left right ugraph)))
 ;;