diff options
| author | filliatr | 2003-07-18 12:25:55 +0000 |
|---|---|---|
| committer | filliatr | 2003-07-18 12:25:55 +0000 |
| commit | f311611616a2fd2ef5b6d10cfc0ae457a6b92a33 (patch) | |
| tree | d6ce6eb590fde54cddf45c568f129afacb3b5142 | |
| parent | 6a3b1ca9467a090b87d5ee98b441020e05f967d8 (diff) | |
Coq.Init.Logic.eq au lieu de eq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4239 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 180596d8d6..24fd54266c 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -22,7 +22,7 @@ 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 ? $p $c) ] +| form_eq [ expr($p) "=" expr($c) ] -> [ (Coq.Init.Logic.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) ] @@ -30,7 +30,7 @@ with formula : constr := (*| 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 ? $p $c)/\(eq ? $c $c1) ] + -> [ (Coq.Init.Logic.eq ? $p $c)/\(Coq.Init.Logic.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) ] @@ -39,8 +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 ? $p $c) ] +(*| form_neq [ expr($p) "<>" expr($c) ] -> [ ~(Coq.Init.Logic.eq Z $p $c) ]*) +| form_neq [ expr($p) "<>" expr($c) ] -> [ ~(Coq.Init.Logic.eq ? $p $c) ] | form_comp [ expr($p) "?=" expr($c) ] -> [ (Zcompare $p $c) ] with expr : constr := |