From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 18 Nov 2010 10:45:50 +0000 (+0000)
Subject: - auto now uses the equality of the new library
X-Git-Tag: make_still_working~2693
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c6aeb873c1c35f6ddf22dfec9ef19977ab53a0f8;p=helm.git

- auto now uses the equality of the new library
---

diff --git a/matita/components/ng_paramodulation/nCicBlob.ml b/matita/components/ng_paramodulation/nCicBlob.ml
index d9679bf3a..e141272af 100644
--- a/matita/components/ng_paramodulation/nCicBlob.ml
+++ b/matita/components/ng_paramodulation/nCicBlob.ml
@@ -14,8 +14,8 @@
 let eqPref = ref (fun _ -> assert false);;
 let set_eqP t = eqPref := fun _ -> t;;
 
-let default_eqP() = 
-  let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+let default_eqP() =
+  let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in
   let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
     NCic.Const ref
 ;;
diff --git a/matita/components/ng_paramodulation/nCicParamod.ml b/matita/components/ng_paramodulation/nCicParamod.ml
index 16ae66e5d..41d27cab9 100644
--- a/matita/components/ng_paramodulation/nCicParamod.ml
+++ b/matita/components/ng_paramodulation/nCicParamod.ml
@@ -18,6 +18,7 @@ NCicProof.set_default_sig()
 
 let debug _ = ();;
 let print s = prerr_endline (Lazy.force s);; 
+let debug = print;;
 
 module B(C : NCicBlob.NCicContext): Orderings.Blob 
   with type t = NCic.term and type input = NCic.term 
@@ -164,7 +165,6 @@ let is_equation metasenv subst context ty =
     | _ -> false
 ;;
 
-
 (*
 let demodulate rdb metasenv subst context s goal =
   (* let stamp = Unix.gettimeofday () in *)
diff --git a/matita/components/ng_paramodulation/nCicProof.ml b/matita/components/ng_paramodulation/nCicProof.ml
index f840d91f9..f9b60ba26 100644
--- a/matita/components/ng_paramodulation/nCicProof.ml
+++ b/matita/components/ng_paramodulation/nCicProof.ml
@@ -19,19 +19,19 @@ let get_sig = fun x -> !eqsig x;;
 
 let default_sig = function
   | Eq -> 
-      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+      let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in
       let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
         NCic.Const ref
   | EqInd_l -> 
-      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_l.con" in
+      let uri = NUri.uri_of_string "cic:/matita/basics/logic/rewrite_l.con" in
       let ref = NReference.reference_of_spec uri (NReference.Def(1)) in
         NCic.Const ref
   | EqInd_r -> 
-      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_r.con" in
+      let uri = NUri.uri_of_string "cic:/matita/basics/logic/rewrite_r.con" in
       let ref = NReference.reference_of_spec uri (NReference.Def(3)) in
         NCic.Const ref
   | Refl ->
-      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+      let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in
       let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in
         NCic.Const ref
 
diff --git a/matita/components/ng_paramodulation/paramod.ml b/matita/components/ng_paramodulation/paramod.ml
index 86a964c14..7a63dd97a 100644
--- a/matita/components/ng_paramodulation/paramod.ml
+++ b/matita/components/ng_paramodulation/paramod.ml
@@ -13,7 +13,7 @@
 
 let print s = prerr_endline (Lazy.force s) ;; 
 let noprint s = ();;  
-let debug = noprint;;
+let debug = print;;
 
 let monster = 100;;
     
diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 95a9e713d..af1d9f944 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -14,7 +14,7 @@ open Printf
 let print ?(depth=0) s = 
   prerr_endline (String.make depth '\t'^Lazy.force s) 
 let noprint ?(depth=0) _ = () 
-let debug_print = noprint
+let debug_print = print
 
 open Continuationals.Stack
 open NTacStatus
@@ -563,7 +563,7 @@ let smart_apply t unit_eq status g =
   noprint(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
   let eq_coerc =       
     let uri = 
-      NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
+      NUri.uri_of_string "cic:/matita/basics/logic/eq_coerc.con" in
     let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
       NCic.Const ref
   in