X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fplus.ma;h=fbb3fcc90b76e4ceb7b037336f3393336ccffea3;hb=08791e80816548121e81e04d3ead8c9a5171d033;hp=1a43e216f7f1a86f2c80713f39db3f13f7ab637f;hpb=244d65f63ca6a736b871f9f91328fe8c5524ff05;p=helm.git

diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma
index 1a43e216f..fbb3fcc90 100644
--- a/helm/matita/library/nat/plus.ma
+++ b/helm/matita/library/nat/plus.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/plus.ma".
+set "baseuri" "cic:/matita/nat/plus".
 
 include "logic/equality.ma".
 include "nat/nat.ma".
@@ -73,4 +73,4 @@ assumption.
 qed.
 
 theorem inj_plus_l: \forall p,n,m:nat.eq nat (plus n p) (plus m p) \to (eq nat n m)
-\def injective_plus_l.
\ No newline at end of file
+\def injective_plus_l.