X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=5ccd8741247ffa0a030893fa26ca9803342f08af;hb=ab44166935d77276c04fcce50aa8281292776e29;hp=eeffd9f1a8bd5985c3071c969c4a28b9da3c03b1;hpb=d622a1ce338d9db774ddc8b98fa58cdcec7b22e5;p=helm.git

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index eeffd9f1a..5ccd87412 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -373,8 +373,10 @@ let replace_metas (* context *) term =
   in
   aux term
 ;;
+*)
 
 
+(*
 let restore_metas (* context *) term =
   let module C = Cic in
   let rec aux = function
@@ -413,8 +415,9 @@ let restore_metas (* context *) term =
   in
   aux term
 ;;
+*)
 
-
+(*
 let rec restore_subst (* context *) subst =
   List.map
     (fun (i, (c, t, ty)) ->
@@ -477,7 +480,7 @@ let unification_simple metasenv context t1 t2 ugraph =
     | C.Meta (i, _), C.Meta (j, _) when i > j ->
         unif subst menv t s
     | C.Meta _, t when occurs_check subst s t ->
-        raise (U.UnificationFailure "Inference.unification.unif")
+        raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
     | C.Meta (i, l), t -> (
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
@@ -497,16 +500,16 @@ 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 "Inference.unification.unif")
+        raise (U.UnificationFailure (U.failure_msg_of_string "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 "Inference.unification.unif")
+          raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
       )
-    | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
+    | _, _ -> raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
   in
   let subst, menv = unif [] metasenv t1 t2 in
   let menv =
@@ -1052,7 +1055,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 (*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
               let (head, newmetas, args, newmeta) =
                 ProofEngineHelpers.saturate_term newmeta []
-                  context (S.lift index term)
+                  context (S.lift index term) 0
               in
               let p =
                 if List.length args = 0 then
@@ -1114,6 +1117,10 @@ let equations_blacklist =
       "cic:/Coq/Init/Logic/sym_eq.con";
 (*       "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *)
 (*       "cic:/Coq/Init/Peano/mult_n_Sm.con"; *)
+
+      (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
+         perche' questo cacchio di teorema rompe le scatole :'( *)
+      "cic:/Rocq/SUBST/comparith/mult_n_2.con"; 
     ]
 ;;
 
@@ -1124,6 +1131,7 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
   let candidates =
     List.fold_left
       (fun l uri ->
+	let suri = UriManager.string_of_uri uri in
          if UriManager.UriSet.mem uri equations_blacklist then
            l
          else
@@ -1148,12 +1156,12 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
     | (term, termty)::tl ->
         debug_print (
           Printf.sprintf "Examining: %s (%s)"
-            (CicPp.ppterm term) (CicPp.ppterm termty));
+            (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty));
         let res, newmeta = 
           match termty with
           | C.Prod (name, s, t) ->
               let head, newmetas, args, newmeta =
-                ProofEngineHelpers.saturate_term newmeta [] context termty
+                ProofEngineHelpers.saturate_term newmeta [] context termty 0
               in
               let p =
                 if List.length args = 0 then