From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 26 Oct 2010 13:20:32 +0000 (+0000)
Subject: Last commit made matita FTBFS. Fixed.
X-Git-Tag: make_still_working~2765
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e14fdca3a845ad0b88a34497f41472c3e7f8473b;p=helm.git

Last commit made matita FTBFS. Fixed.
---

diff --git a/matita/components/METAS/meta.helm-ng_kernel.src b/matita/components/METAS/meta.helm-ng_kernel.src
index df165a210..f35420375 100644
--- a/matita/components/METAS/meta.helm-ng_kernel.src
+++ b/matita/components/METAS/meta.helm-ng_kernel.src
@@ -1,4 +1,4 @@
-requires=""
+requires="helm-extlib"
 version="0.0.1"
 archive(byte)="ng_kernel.cma"
 archive(native)="ng_kernel.cmxa"
diff --git a/matita/components/binaries/test_parser/Makefile b/matita/components/binaries/test_parser/Makefile
index 7d5981a57..52f1a4fea 100644
--- a/matita/components/binaries/test_parser/Makefile
+++ b/matita/components/binaries/test_parser/Makefile
@@ -6,11 +6,11 @@ INTERFACE_FILES =
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) 
 EXTRA_OBJECTS_TO_INSTALL =
 EXTRA_OBJECTS_TO_CLEAN = \
-	test_parser test_parser.opt test_dep test_dep.opt print_grammar print_grammar.opt
+	test_parser test_parser.opt test_dep test_dep.opt
 
-all: test_parser test_dep print_grammar
+all: test_parser test_dep
 	$(H)echo -n
-opt: test_parser.opt test_dep.opt print_grammar.opt
+opt: test_parser.opt test_dep.opt
 	$(H)echo -n
 
 test_parser: test_parser.ml
@@ -33,19 +33,9 @@ test_dep.opt: test_dep.ml
 	$(H)$(OCAMLFIND) ocamlopt \
 		-I ../../tactics/paramodulation/ -thread -package "$(REQUIRES)" -linkpkg -o $@ $<
 
-print_grammar: print_grammar.ml
-	$(H)echo "    OCAMLC $<"
-	$(H)$(OCAMLFIND) ocamlc \
-		-I ../../tactics/paramodulation/ -rectypes -thread -package "$(REQUIRES)" -linkpkg -o $@ $<
-
-print_grammar.opt: print_grammar.ml
-	$(H)echo "    OCAMLOPT $<"
-	$(H)$(OCAMLFIND) ocamlopt \
-		-I ../../tactics/paramodulation/ -thread -package "$(REQUIRES)" -linkpkg -o $@ $<
-
 clean:
 	$(H)rm -f *.cm[iox] *.a *.o
-	$(H)rm -f test_parser test_parser.opt test_dep test_dep.opt print_grammar print_grammar.opt
+	$(H)rm -f test_parser test_parser.opt test_dep test_dep.opt
 
 depend:
 depend.opt:
diff --git a/matita/components/binaries/test_parser/print_grammar.ml b/matita/components/binaries/test_parser/print_grammar.ml
deleted file mode 100644
index 893a3f53c..000000000
--- a/matita/components/binaries/test_parser/print_grammar.ml
+++ /dev/null
@@ -1,275 +0,0 @@
-(* Copyright (C) 2005, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-open Gramext 
-
-let rec flatten_tree = function
-  | DeadEnd -> []
-  | LocAct _ -> [[]]
-  | Node {node = n; brother = b; son = s} ->
-      List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b
-
-let tex_of_unicode s = s
-
-let rec clean_dummy_desc = function
-  | Dlevels l -> Dlevels (clean_levels l)
-  | x -> x
-
-and clean_levels = function
-  | [] -> []
-  | l :: tl -> clean_level l @ clean_levels tl
-  
-and clean_level = function
-  | x -> 
-      let pref = clean_tree x.lprefix in
-      let suff = clean_tree x.lsuffix in
-      match pref,suff with
-      | DeadEnd, DeadEnd -> []
-      | _ -> [{x with lprefix = pref; lsuffix = suff}]
-  
-and clean_tree = function
-  | Node n -> clean_node n
-  | x -> x
-  
-and clean_node = function
-  | {node=node;son=son;brother=brother} ->
-      let bn = is_symbol_dummy node in
-      let bs = is_tree_dummy son in
-      let bb = is_tree_dummy brother in
-      let son = if bs then DeadEnd else son in
-      let brother = if bb then DeadEnd else brother in
-      if bb && bs && bn then
-        DeadEnd
-      else 
-        if bn then 
-          Node {node=Sself;son=son;brother=brother}
-        else
-          Node {node=node;son=son;brother=brother}
-
-and is_level_dummy = function
-  | {lsuffix=lsuffix;lprefix=lprefix} -> 
-      is_tree_dummy lsuffix && is_tree_dummy lprefix
-  
-and is_desc_dummy = function
-  | Dlevels l -> List.for_all is_level_dummy l
-  | Dparser _ -> true
-  
-and is_entry_dummy = function
-  | {edesc=edesc} -> is_desc_dummy edesc
-  
-and is_symbol_dummy = function
-  | Stoken ("DUMMY", _) -> true
-  | Stoken _ -> false
-  | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
-  | Snterm e | Snterml (e, _) -> is_entry_dummy e
-  | Slist1 x | Slist0 x -> is_symbol_dummy x
-  | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
-  | Sopt x -> is_symbol_dummy x
-  | Sself | Snext -> false
-  | Stree t -> is_tree_dummy t
-  | _ -> assert false
-  
-and is_tree_dummy = function
-  | Node {node=node} -> is_symbol_dummy node 
-  | _ -> true
-
-let needs_brackets t =
-  let rec count_brothers = function 
-    | Node {brother = brother} -> 1 + count_brothers brother
-    | _ -> 0
-  in
-  count_brothers t > 1
-
-let visit_description desc fmt self = 
-  let skip s = true in
-  let inline s = List.mem s [ "int" ] in
-  
-  let rec visit_entry e ?level todo is_son  =
-    let { ename = ename; edesc = desc } = e in 
-    if inline ename then 
-      visit_desc desc todo is_son 
-    else
-      begin
-       (match level with
-       | None -> Format.fprintf fmt "%s " ename;
-       | Some _ -> Format.fprintf fmt "%s " ename;);
-          if skip ename then
-            todo
-          else
-            todo @ [e]
-      end
-      
-  and visit_desc d todo is_son  =
-    match d with
-    | Dlevels l ->
-        List.fold_left  
-        (fun acc l -> 
-           Format.fprintf fmt "@ ";
-           visit_level l acc is_son ) 
-          todo l;
-    | Dparser _ -> todo
-    
-  and visit_level l todo is_son  =
-    let { lname = name ; lsuffix = suff ; lprefix = pref } = l in
-        visit_tree name
-          (List.map 
-            (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref)
-          todo is_son  
-    
-  and visit_tree name t todo is_son  = 
-    if List.for_all (List.for_all is_symbol_dummy) t then todo else (
-    Format.fprintf fmt "@[<v>";
-    (match name with 
-    |Some name -> Format.fprintf fmt "Precedence %s:@ " name 
-    | None -> ());
-    Format.fprintf fmt "@[<v>";
-    let todo = 
-      List.fold_left 
-       (fun acc x ->
-         if List.for_all is_symbol_dummy x then todo else (
-         Format.fprintf fmt "@[<h> | ";
-         let todo = 
-           List.fold_left 
-            (fun acc x -> 
-               let todo = visit_symbol x acc true in
-               Format.fprintf fmt "@ ";
-               todo)
-            acc x
-         in
-         Format.fprintf fmt "@]@ ";
-         todo))
-       todo t 
-    in
-    Format.fprintf fmt "@]";
-    Format.fprintf fmt "@]";
-    todo)
-    
-  and visit_symbol s todo is_son  =
-    match s with
-    | Smeta (name, sl, _) -> 
-        Format.fprintf fmt "%s " name;
-        List.fold_left (
-          fun acc s -> 
-            let todo = visit_symbol s acc is_son  in
-            if is_son then
-              Format.fprintf fmt "@ ";
-            todo) 
-        todo sl
-    | Snterm entry -> visit_entry entry todo is_son  
-    | Snterml (entry,level) -> visit_entry entry ~level todo is_son 
-    | Slist0 symbol -> 
-        Format.fprintf fmt "{@[<hov2> ";
-        let todo = visit_symbol symbol todo is_son in
-        Format.fprintf fmt "@]} @ ";
-        todo
-    | Slist0sep (symbol,sep) ->
-        Format.fprintf fmt "[@[<hov2> ";
-        let todo = visit_symbol symbol todo is_son in
-        Format.fprintf fmt "{@[<hov2> ";
-        let todo = visit_symbol sep todo is_son in
-        Format.fprintf fmt " ";
-        let todo = visit_symbol symbol todo is_son in
-        Format.fprintf fmt "@]} @]] @ ";
-        todo
-    | Slist1 symbol -> 
-        Format.fprintf fmt "{@[<hov2> ";
-        let todo = visit_symbol symbol todo is_son in
-        Format.fprintf fmt "@]}+ @ ";
-        todo 
-    | Slist1sep (symbol,sep) ->
-        let todo = visit_symbol symbol todo is_son  in
-        Format.fprintf fmt "{@[<hov2> ";
-        let todo = visit_symbol sep todo is_son in
-        let todo = visit_symbol symbol todo is_son in
-        Format.fprintf fmt "@]} @ ";
-        todo
-    | Sopt symbol -> 
-        Format.fprintf fmt "[@[<hov2> ";
-        let todo = visit_symbol symbol todo is_son in
-        Format.fprintf fmt "@]] @ ";
-        todo
-    | Sself -> Format.fprintf fmt "%s " self; todo
-    | Snext -> Format.fprintf fmt "next "; todo
-    | Stoken pattern -> 
-        let constructor, keyword = pattern in
-        if keyword = "" then
-          (if constructor <> "DUMMY" then
-            Format.fprintf fmt "`%s' " constructor)
-        else
-          Format.fprintf fmt "%s " (tex_of_unicode keyword);
-        todo
-    | Stree tree ->
-        visit_tree None (flatten_tree tree) todo is_son 
-    | _ -> assert false
-  in
-  visit_desc desc [] false
-;;
-
-
-let rec visit_entries fmt todo pped =
-  match todo with
-  | [] -> ()
-  | hd :: tl -> 
-      let todo =
-        if not (List.memq hd pped) then
-          begin
-            let { ename = ename; edesc = desc } = hd in 
-            Format.fprintf fmt "@[<hv 2>%s ::= " ename;
-            let desc = clean_dummy_desc desc in 
-            let todo = visit_description desc fmt ename @ todo in
-            Format.fprintf fmt "@]\n\n";
-            todo 
-          end
-        else
-          todo
-      in
-      let clean_todo todo =
-        let name_of_entry e = e.ename in
-        let pped = hd :: pped in
-        let todo = tl @ todo in
-        let todo = List.filter (fun e -> not(List.memq e pped)) todo in
-        HExtlib.list_uniq 
-          ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
-          (List.sort 
-            (fun e1 e2 -> 
-              Pervasives.compare (name_of_entry e1) (name_of_entry e2))
-            todo),
-        pped
-      in
-      let todo,pped = clean_todo todo in
-      visit_entries fmt todo pped
-;;
-
-let ebnf_of_term () =
-  let g_entry = Grammar.Entry.obj (CicNotationParser.term ()) in
-  let buff = Buffer.create 100 in
-  let fmt = Format.formatter_of_buffer buff in
-  visit_entries fmt [g_entry] [];
-  Format.fprintf fmt "@?";
-  let s = Buffer.contents buff in
-  s
-;;
diff --git a/matita/components/grafite_parser/Makefile b/matita/components/grafite_parser/Makefile
index 45ee2aa0f..5583ecb8a 100644
--- a/matita/components/grafite_parser/Makefile
+++ b/matita/components/grafite_parser/Makefile
@@ -7,7 +7,7 @@ INTERFACE_FILES = 			\
 	cicNotation2.mli		\
 	nEstatus.mli			\
 	grafiteDisambiguate.mli 	\
-	print_grammar.mli 		\
+	print_grammar.mli 	\
 	$(NULL)
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 
diff --git a/matita/components/grafite_parser/print_grammar.ml b/matita/components/grafite_parser/print_grammar.ml
new file mode 100644
index 000000000..893a3f53c
--- /dev/null
+++ b/matita/components/grafite_parser/print_grammar.ml
@@ -0,0 +1,275 @@
+(* Copyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+open Gramext 
+
+let rec flatten_tree = function
+  | DeadEnd -> []
+  | LocAct _ -> [[]]
+  | Node {node = n; brother = b; son = s} ->
+      List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b
+
+let tex_of_unicode s = s
+
+let rec clean_dummy_desc = function
+  | Dlevels l -> Dlevels (clean_levels l)
+  | x -> x
+
+and clean_levels = function
+  | [] -> []
+  | l :: tl -> clean_level l @ clean_levels tl
+  
+and clean_level = function
+  | x -> 
+      let pref = clean_tree x.lprefix in
+      let suff = clean_tree x.lsuffix in
+      match pref,suff with
+      | DeadEnd, DeadEnd -> []
+      | _ -> [{x with lprefix = pref; lsuffix = suff}]
+  
+and clean_tree = function
+  | Node n -> clean_node n
+  | x -> x
+  
+and clean_node = function
+  | {node=node;son=son;brother=brother} ->
+      let bn = is_symbol_dummy node in
+      let bs = is_tree_dummy son in
+      let bb = is_tree_dummy brother in
+      let son = if bs then DeadEnd else son in
+      let brother = if bb then DeadEnd else brother in
+      if bb && bs && bn then
+        DeadEnd
+      else 
+        if bn then 
+          Node {node=Sself;son=son;brother=brother}
+        else
+          Node {node=node;son=son;brother=brother}
+
+and is_level_dummy = function
+  | {lsuffix=lsuffix;lprefix=lprefix} -> 
+      is_tree_dummy lsuffix && is_tree_dummy lprefix
+  
+and is_desc_dummy = function
+  | Dlevels l -> List.for_all is_level_dummy l
+  | Dparser _ -> true
+  
+and is_entry_dummy = function
+  | {edesc=edesc} -> is_desc_dummy edesc
+  
+and is_symbol_dummy = function
+  | Stoken ("DUMMY", _) -> true
+  | Stoken _ -> false
+  | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
+  | Snterm e | Snterml (e, _) -> is_entry_dummy e
+  | Slist1 x | Slist0 x -> is_symbol_dummy x
+  | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
+  | Sopt x -> is_symbol_dummy x
+  | Sself | Snext -> false
+  | Stree t -> is_tree_dummy t
+  | _ -> assert false
+  
+and is_tree_dummy = function
+  | Node {node=node} -> is_symbol_dummy node 
+  | _ -> true
+
+let needs_brackets t =
+  let rec count_brothers = function 
+    | Node {brother = brother} -> 1 + count_brothers brother
+    | _ -> 0
+  in
+  count_brothers t > 1
+
+let visit_description desc fmt self = 
+  let skip s = true in
+  let inline s = List.mem s [ "int" ] in
+  
+  let rec visit_entry e ?level todo is_son  =
+    let { ename = ename; edesc = desc } = e in 
+    if inline ename then 
+      visit_desc desc todo is_son 
+    else
+      begin
+       (match level with
+       | None -> Format.fprintf fmt "%s " ename;
+       | Some _ -> Format.fprintf fmt "%s " ename;);
+          if skip ename then
+            todo
+          else
+            todo @ [e]
+      end
+      
+  and visit_desc d todo is_son  =
+    match d with
+    | Dlevels l ->
+        List.fold_left  
+        (fun acc l -> 
+           Format.fprintf fmt "@ ";
+           visit_level l acc is_son ) 
+          todo l;
+    | Dparser _ -> todo
+    
+  and visit_level l todo is_son  =
+    let { lname = name ; lsuffix = suff ; lprefix = pref } = l in
+        visit_tree name
+          (List.map 
+            (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref)
+          todo is_son  
+    
+  and visit_tree name t todo is_son  = 
+    if List.for_all (List.for_all is_symbol_dummy) t then todo else (
+    Format.fprintf fmt "@[<v>";
+    (match name with 
+    |Some name -> Format.fprintf fmt "Precedence %s:@ " name 
+    | None -> ());
+    Format.fprintf fmt "@[<v>";
+    let todo = 
+      List.fold_left 
+       (fun acc x ->
+         if List.for_all is_symbol_dummy x then todo else (
+         Format.fprintf fmt "@[<h> | ";
+         let todo = 
+           List.fold_left 
+            (fun acc x -> 
+               let todo = visit_symbol x acc true in
+               Format.fprintf fmt "@ ";
+               todo)
+            acc x
+         in
+         Format.fprintf fmt "@]@ ";
+         todo))
+       todo t 
+    in
+    Format.fprintf fmt "@]";
+    Format.fprintf fmt "@]";
+    todo)
+    
+  and visit_symbol s todo is_son  =
+    match s with
+    | Smeta (name, sl, _) -> 
+        Format.fprintf fmt "%s " name;
+        List.fold_left (
+          fun acc s -> 
+            let todo = visit_symbol s acc is_son  in
+            if is_son then
+              Format.fprintf fmt "@ ";
+            todo) 
+        todo sl
+    | Snterm entry -> visit_entry entry todo is_son  
+    | Snterml (entry,level) -> visit_entry entry ~level todo is_son 
+    | Slist0 symbol -> 
+        Format.fprintf fmt "{@[<hov2> ";
+        let todo = visit_symbol symbol todo is_son in
+        Format.fprintf fmt "@]} @ ";
+        todo
+    | Slist0sep (symbol,sep) ->
+        Format.fprintf fmt "[@[<hov2> ";
+        let todo = visit_symbol symbol todo is_son in
+        Format.fprintf fmt "{@[<hov2> ";
+        let todo = visit_symbol sep todo is_son in
+        Format.fprintf fmt " ";
+        let todo = visit_symbol symbol todo is_son in
+        Format.fprintf fmt "@]} @]] @ ";
+        todo
+    | Slist1 symbol -> 
+        Format.fprintf fmt "{@[<hov2> ";
+        let todo = visit_symbol symbol todo is_son in
+        Format.fprintf fmt "@]}+ @ ";
+        todo 
+    | Slist1sep (symbol,sep) ->
+        let todo = visit_symbol symbol todo is_son  in
+        Format.fprintf fmt "{@[<hov2> ";
+        let todo = visit_symbol sep todo is_son in
+        let todo = visit_symbol symbol todo is_son in
+        Format.fprintf fmt "@]} @ ";
+        todo
+    | Sopt symbol -> 
+        Format.fprintf fmt "[@[<hov2> ";
+        let todo = visit_symbol symbol todo is_son in
+        Format.fprintf fmt "@]] @ ";
+        todo
+    | Sself -> Format.fprintf fmt "%s " self; todo
+    | Snext -> Format.fprintf fmt "next "; todo
+    | Stoken pattern -> 
+        let constructor, keyword = pattern in
+        if keyword = "" then
+          (if constructor <> "DUMMY" then
+            Format.fprintf fmt "`%s' " constructor)
+        else
+          Format.fprintf fmt "%s " (tex_of_unicode keyword);
+        todo
+    | Stree tree ->
+        visit_tree None (flatten_tree tree) todo is_son 
+    | _ -> assert false
+  in
+  visit_desc desc [] false
+;;
+
+
+let rec visit_entries fmt todo pped =
+  match todo with
+  | [] -> ()
+  | hd :: tl -> 
+      let todo =
+        if not (List.memq hd pped) then
+          begin
+            let { ename = ename; edesc = desc } = hd in 
+            Format.fprintf fmt "@[<hv 2>%s ::= " ename;
+            let desc = clean_dummy_desc desc in 
+            let todo = visit_description desc fmt ename @ todo in
+            Format.fprintf fmt "@]\n\n";
+            todo 
+          end
+        else
+          todo
+      in
+      let clean_todo todo =
+        let name_of_entry e = e.ename in
+        let pped = hd :: pped in
+        let todo = tl @ todo in
+        let todo = List.filter (fun e -> not(List.memq e pped)) todo in
+        HExtlib.list_uniq 
+          ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
+          (List.sort 
+            (fun e1 e2 -> 
+              Pervasives.compare (name_of_entry e1) (name_of_entry e2))
+            todo),
+        pped
+      in
+      let todo,pped = clean_todo todo in
+      visit_entries fmt todo pped
+;;
+
+let ebnf_of_term () =
+  let g_entry = Grammar.Entry.obj (CicNotationParser.term ()) in
+  let buff = Buffer.create 100 in
+  let fmt = Format.formatter_of_buffer buff in
+  visit_entries fmt [g_entry] [];
+  Format.fprintf fmt "@?";
+  let s = Buffer.contents buff in
+  s
+;;
diff --git a/matita/components/ng_paramodulation/nCicBlob.ml b/matita/components/ng_paramodulation/nCicBlob.ml
index fb9ee6245..d9679bf3a 100644
--- a/matita/components/ng_paramodulation/nCicBlob.ml
+++ b/matita/components/ng_paramodulation/nCicBlob.ml
@@ -33,18 +33,6 @@ let setoid_eq =
 
 let set_default_eqP() = eqPref := default_eqP
 
-let set_reference_of_oxuri f = 
-  let eqnew = function 
-      _ -> 
-	let r = f(UriManager.uri_of_string 
-          "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
-	in
-	  NCic.Const r
-  in
-    eqPref := eqnew
-;;
-
-
 module type NCicContext =
   sig
     val metasenv : NCic.metasenv
diff --git a/matita/components/ng_paramodulation/nCicBlob.mli b/matita/components/ng_paramodulation/nCicBlob.mli
index a8b6a7b7e..5d0c7ae2b 100644
--- a/matita/components/ng_paramodulation/nCicBlob.mli
+++ b/matita/components/ng_paramodulation/nCicBlob.mli
@@ -11,7 +11,6 @@
 
 (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *)
 
-val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
 val set_eqP: NCic.term -> unit
 val set_default_eqP: unit -> unit
 
diff --git a/matita/components/ng_paramodulation/nCicProof.ml b/matita/components/ng_paramodulation/nCicProof.ml
index c5290694b..f840d91f9 100644
--- a/matita/components/ng_paramodulation/nCicProof.ml
+++ b/matita/components/ng_paramodulation/nCicProof.ml
@@ -39,32 +39,6 @@ let set_default_sig () =
   (*prerr_endline "setting default sig";*)
   eqsig := default_sig
 
-let set_reference_of_oxuri reference_of_oxuri = 
-  prerr_endline "setting oxuri in nCicProof";
-  let nsig = function
-    | Eq -> 
-        NCic.Const
-          (reference_of_oxuri 
-             (UriManager.uri_of_string 
-                "cic:/matita/logic/equality/eq.ind#xpointer(1/1)"))  
-    | EqInd_l -> 
-        NCic.Const
-          (reference_of_oxuri 
-             (UriManager.uri_of_string 
-                "cic:/matita/logic/equality/eq_ind.con"))
-    | EqInd_r -> 
-        NCic.Const
-          (reference_of_oxuri 
-             (UriManager.uri_of_string 
-                "cic:/matita/logic/equality/eq_elim_r.con"))
-    | Refl ->
-        NCic.Const
-          (reference_of_oxuri 
-             (UriManager.uri_of_string 
-                "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)"))
-  in eqsig:= nsig
-  ;;
-
 (* let debug c r = prerr_endline r; c *)
 let debug c _ = c;;
 
diff --git a/matita/components/ng_paramodulation/nCicProof.mli b/matita/components/ng_paramodulation/nCicProof.mli
index 2aa0a8dd8..f1e1e3b32 100644
--- a/matita/components/ng_paramodulation/nCicProof.mli
+++ b/matita/components/ng_paramodulation/nCicProof.mli
@@ -13,7 +13,6 @@
 
 type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
 
-val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
 val set_default_sig: unit -> unit
 val get_sig: eq_sig_type -> NCic.term