diff options
| author | barras | 2003-10-22 10:35:04 +0000 |
|---|---|---|
| committer | barras | 2003-10-22 10:35:04 +0000 |
| commit | 6475388a91c899e8bcf7b69b223180025d4f85ff (patch) | |
| tree | 6031dc6e72bb676fa9d9e4f9f2be8ab50c1ca2e3 /theories/Num | |
| parent | 9da09a4da10aa36699538bde01086172c64689eb (diff) | |
reorganisation des niveaux (ex: = est a 70)
Hint Destruct: syntaxe similaire aux autres hints...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Num')
| -rw-r--r-- | theories/Num/NSyntax.v | 10 | ||||
| -rw-r--r-- | theories/Num/NeqDef.v | 2 | ||||
| -rw-r--r-- | theories/Num/NeqParams.v | 2 |
3 files changed, 7 insertions, 7 deletions
diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v index 55912fdda5..00d7a032d4 100644 --- a/theories/Num/NSyntax.v +++ b/theories/Num/NSyntax.v @@ -10,12 +10,12 @@ Require Export Params. -Infix 6 "<" lt V8only 50. -Infix 6 "<=" le V8only 50. -Infix 6 ">" gt V8only 50. -Infix 6 ">=" ge V8only 50. +Infix 6 "<" lt V8only 70. +Infix 6 "<=" le V8only 70. +Infix 6 ">" gt V8only 70. +Infix 6 ">=" ge V8only 70. -(*i Infix 7 "+" plus V8only 40. i*) +(*i Infix 7 "+" plus V8only 50. i*) Grammar constr lassoc_constr4 := squash_sum diff --git a/theories/Num/NeqDef.v b/theories/Num/NeqDef.v index 0e00294223..ff5bc3e67c 100644 --- a/theories/Num/NeqDef.v +++ b/theories/Num/NeqDef.v @@ -15,7 +15,7 @@ Require EqParams. Require EqAxioms. Definition neq : N -> N -> Prop := [x,y] ~(x=y). -Infix 6 "<>" neq V8only 50. +Infix 6 "<>" neq V8only 70. (* Proofs of axioms *) Lemma eq_not_neq : (x,y:N)x=y->~(x<>y). diff --git a/theories/Num/NeqParams.v b/theories/Num/NeqParams.v index 7f7a5139e4..4b76771669 100644 --- a/theories/Num/NeqParams.v +++ b/theories/Num/NeqParams.v @@ -15,7 +15,7 @@ Require Export Params. Parameter neq : N -> N -> Prop. -Infix 6 "<>" neq V8only 50. +Infix 6 "<>" neq V8only 70. |