diff options
| author | monate | 2003-05-07 16:56:52 +0000 |
|---|---|---|
| committer | monate | 2003-05-07 16:56:52 +0000 |
| commit | dd53f04b22a4ba3b539fb25ba23d7757e5af2349 (patch) | |
| tree | b3e7126afd59e26921e7d01f40f6fcbbcfa4ba34 /theories/ZArith | |
| parent | 0980569e174509e6718c96675c1aea1f82ce79ae (diff) | |
coqide: toolbar/autosave
Hugo: Suppression du type dans les notations == et <> entre
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3992 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 757b539ab6..cd116ecb0a 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -21,13 +21,16 @@ with negnumber := with formula : constr := form_expr [ expr($p) ] -> [$p] -| form_eq [ expr($p) "=" expr($c) ] -> [ (eq Z $p $c) ] +(*| form_eq [ expr($p) "=" expr($c) ] -> [ (eq Z $p $c) ]*) +| form_eq [ expr($p) "=" expr($c) ] -> [ (eq ? $p $c) ] | form_le [ expr($p) "<=" expr($c) ] -> [ (Zle $p $c) ] | form_lt [ expr($p) "<" expr($c) ] -> [ (Zlt $p $c) ] | form_ge [ expr($p) ">=" expr($c) ] -> [ (Zge $p $c) ] | form_gt [ expr($p) ">" expr($c) ] -> [ (Zgt $p $c) ] +(*| form_eq_eq [ expr($p) "=" expr($c) "=" expr($c1) ] + -> [ (eq Z $p $c)/\(eq Z $c $c1) ]*) | form_eq_eq [ expr($p) "=" expr($c) "=" expr($c1) ] - -> [ (eq Z $p $c)/\(eq Z $c $c1) ] + -> [ (eq ? $p $c)/\(eq ? $c $c1) ] | form_le_le [ expr($p) "<=" expr($c) "<=" expr($c1) ] -> [ (Zle $p $c)/\(Zle $c $c1) ] | form_le_lt [ expr($p) "<=" expr($c) "<" expr($c1) ] @@ -36,7 +39,8 @@ with formula : constr := -> [ (Zlt $p $c)/\(Zle $c $c1) ] | form_lt_lt [ expr($p) "<" expr($c) "<" expr($c1) ] -> [ (Zlt $p $c)/\(Zlt $c $c1) ] -| form_neq [ expr($p) "<>" expr($c) ] -> [ ~(eq Z $p $c) ] +(*| form_neq [ expr($p) "<>" expr($c) ] -> [ ~(eq Z $p $c) ]*) +| form_neq [ expr($p) "<>" expr($c) ] -> [ ~(eq ? $p $c) ] | form_comp [ expr($p) "?=" expr($c) ] -> [ (Zcompare $p $c) ] with expr : constr := |