Bug fixed: the generated elimination principles used to have Anonymous

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

diff --git a/helm/matita/library/nat/orders_op.ma b/helm/matita/library/nat/orders_op.ma
index dbd48fa8852f6d91e2c31d33a675eeb4cb729e1d..801e123d2c901a65c7894c04fe71c9e5920700f6 100644 (file)
--- a/helm/matita/library/nat/orders_op.ma
+++ b/helm/matita/library/nat/orders_op.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/orders_op.ma".
+set "baseuri" "cic:/matita/nat/orders_op".
 
 include "higher_order_defs/functions.ma".
 include "nat/times.ma".