Bug fixed: the generated elimination principles used to have Anonymous

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

diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma
index f9c731bb0e4c85447cffb3d460358ddb9809d2c8..44f73b71a080b6e253d49b5dfbb2e1b622d45174 100644 (file)
--- a/helm/matita/library/nat/times.ma
+++ b/helm/matita/library/nat/times.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/times.ma".
+set "baseuri" "cic:/matita/nat/times".
 
 include "logic/equality.ma".
 include "nat/nat.ma".