From febd89f8a2b61f958e149ed630f5c991eb7d9661 Mon Sep 17 00:00:00 2001 From: Alberto Griggio 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