diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-21 17:37:19 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-21 17:37:19 +0000 |
| commit | fa6f9f8441694f9af5dce403101fe6114876853c (patch) | |
| tree | f6e2341581304e58a2de28687c85110f57a2e305 /theories/Num | |
| parent | 3ad605604d6715b238cb4f640d855f4fc0238ab4 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Num')
| -rw-r--r-- | theories/Num/EqParams.v | 4 | ||||
| -rw-r--r-- | theories/Num/NSyntax.v | 12 | ||||
| -rw-r--r-- | theories/Num/NeqDef.v | 2 | ||||
| -rw-r--r-- | theories/Num/NeqParams.v | 2 |
4 files changed, 10 insertions, 10 deletions
diff --git a/theories/Num/EqParams.v b/theories/Num/EqParams.v index f7fec9f92..c8fd74fcb 100644 --- a/theories/Num/EqParams.v +++ b/theories/Num/EqParams.v @@ -14,7 +14,7 @@ Require Export Params. Parameter eqN:N->N->Prop. -(*i Infix 6 "=" eqN. i*) +(*i Infix 6 "=" eqN V8only 50. i*) Grammar constr constr1 := eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ]. @@ -22,4 +22,4 @@ eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ]. Syntax constr level 1: equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ] -.
\ No newline at end of file +. diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v index 7787c1f03..55912fdda 100644 --- a/theories/Num/NSyntax.v +++ b/theories/Num/NSyntax.v @@ -10,12 +10,12 @@ Require Export Params. -Infix 6 "<" lt. -Infix 6 "<=" le. -Infix 6 ">" gt. -Infix 6 ">=" ge. +Infix 6 "<" lt V8only 50. +Infix 6 "<=" le V8only 50. +Infix 6 ">" gt V8only 50. +Infix 6 ">=" ge V8only 50. -(*i Infix 7 "+" plus. i*) +(*i Infix 7 "+" plus V8only 40. i*) Grammar constr lassoc_constr4 := squash_sum @@ -32,4 +32,4 @@ Grammar constr lassoc_constr4 := Syntax constr level 4: sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ] -.
\ No newline at end of file +. diff --git a/theories/Num/NeqDef.v b/theories/Num/NeqDef.v index 9d310a039..0e0029422 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. +Infix 6 "<>" neq V8only 50. (* 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 4e651954f..7f7a5139e 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. +Infix 6 "<>" neq V8only 50. |