- auto now uses the equality of the new library

[helm.git] / matita / components / ng_tactics / nnAuto.ml

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 95a9e713d7390a0c2b424deaf3562ae304588336..af1d9f944c2757a9dfaf44102847045f2e03403d 100644 (file)
--- 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