From febd89f8a2b61f958e149ed630f5c991eb7d9661 Mon Sep 17 00:00:00 2001
From: Alberto Griggio <griggio@fbk.eu>
Date: Tue, 6 Sep 2005 14:18:12 +0000
Subject: [PATCH] added dirty hack to blacklist mult_n_2, which causes
 troubles... :-(

---
 helm/ocaml/paramodulation/inference.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index eeffd9f1a..e92117334 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)) ->
@@ -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,7 +1156,7 @@ 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) ->
-- 
2.39.2