- 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 d9679bf3abdd5c36de60622e7f28a367cd9b5328..e141272affa53b058df09ff2179c79070696f339 100644 (file)
--- 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 16ae66e5da45f76259420625ebd2311247899987..41d27cab934794f0df9d658b39aad00c7b93dad4 100644 (file)
--- 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 f840d91f902233642e247cc6fdab1c440c4b0d32..f9b60ba26d916ca14383192c0633789bdd855bc3 100644 (file)
--- 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 86a964c1487f36a7f72deb0c8f2608f621ec2aac..7a63dd97a292150b5e6ee3e4120ba9981cc78827 100644 (file)
--- 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 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