X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=f4466fc1a36abb0ebd1a219dfe7eaf3b5444acd2;hb=7ad16d18416a08382d62747fce4a0ac18ee557e0;hp=95a9e713d7390a0c2b424deaf3562ae304588336;hpb=3ce27112fe93ced5f67cc6af8fc63037eba3f322;p=helm.git diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 95a9e713d..f4466fc1a 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -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