Bug fixed: the generated elimination principles used to have Anonymous

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

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 4fa85a6bb4f6c901a28fcafcff0ad68d5def0a48..0091cb9b09b93ace2834862b1b84d64d7bdd219d 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/minus.ma".
+set "baseuri" "cic:/matita/nat/minus".
 
 include "nat/orders_op.ma".
 include "nat/times.ma".