Bug fixed: the generated elimination principles used to have Anonymous

[helm.git] / helm / matita / library / nat / plus.ma

diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma
index 1a43e216f7f1a86f2c80713f39db3f13f7ab637f..fbb3fcc90b76e4ceb7b037336f3393336ccffea3 100644 (file)
--- 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.