diff options
Diffstat (limited to 'theories/Num/NSyntax.v')
| -rw-r--r-- | theories/Num/NSyntax.v | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v index 488f900e5b..443056fd89 100644 --- a/theories/Num/NSyntax.v +++ b/theories/Num/NSyntax.v @@ -9,18 +9,11 @@ (*s Syntax for arithmetic *) Require Export Params. -Require Export NeqDef. Infix 6 "<" lt. Infix 6 "<=" le. Infix 6 ">" gt. Infix 6 ">=" ge. -Infix 6 "<>" neq. - -(*i Infix 6 "=" eq. i*) - -Grammar constr constr1 := -eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eq $c $c2) ]. (*i Infix 7 "+" plus. i*) @@ -38,7 +31,7 @@ Grammar constr lassoc_constr4 := Syntax constr level 1: - equal [ (eq $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ] + equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ] ; level 4: |