diff options
Diffstat (limited to 'theories/ZArith/Int.v')
| -rw-r--r-- | theories/ZArith/Int.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 3a0d7090d6..62cce1d262 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -220,10 +220,10 @@ Module MoreInt (I:Int). | (?x \/ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPor ex ey) | (~ ?x) => let ex := p2ep x in constr:(EPneg ex) | (eq (A:=Z) ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EPeq ex ey) - | (?x<?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPlt ex ey) - | (?x<=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPle ex ey) - | (?x>?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPgt ex ey) - | (?x>=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPge ex ey) + | (?x < ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPlt ex ey) + | (?x <= ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPle ex ey) + | (?x > ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPgt ex ey) + | (?x >= ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPge ex ey) | ?x => constr:(EPraw x) end. |