Bug fixed: the generated elimination principles used to have Anonymous

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

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 4c1b1a0c4851b65b64140193a626c90c922bb7c0..1939b3c13764e4c9937dbe5af73a3bd09abb0dc2 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/orders.ma".
+set "baseuri" "cic:/matita/nat/orders".
 
 include "logic/connectives.ma".
 include "logic/equality.ma".
@@ -67,7 +67,7 @@ qed.
 
 theorem le_S_S_to_le : \forall n,m:nat. le (S n) (S m) \to le n m.
 intros.change with le (pred (S n)) (pred (S m)).
-elim H.apply le_n.apply trans_le ? (pred x).assumption.
+elim H.apply le_n.apply trans_le ? (pred e2).assumption.
 apply le_pred_n.
 qed.