diff options
Diffstat (limited to 'theories/Init/Peano.v')
| -rwxr-xr-x | theories/Init/Peano.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index fc99d1a48..dcfbe5e99 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -131,7 +131,7 @@ Inductive le [n:nat] : nat -> Prop | le_S : (m:nat)(le n m)->(le n (S m)). Hint constr_le : core v62 := Constructors le. -(* equivalent to : "Hints Resolve le_n le_S : core v62." *) +(*i equivalent to : "Hints Resolve le_n le_S : core v62." i*) Definition lt := [n,m:nat](le (S n) m). Hints Unfold lt : core v62. |