diff options
| author | Maxime Dénès | 2017-06-15 22:00:17 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-15 22:00:17 +0200 |
| commit | 6467119bd15395bb5fae7d9c19dde17293842bd8 (patch) | |
| tree | 809a7156570542f796b4ed94d901a83468d78dc4 /test-suite | |
| parent | 9beec0fc6cc283294bbbda363a3f788ae56347d5 (diff) | |
| parent | 0b5ef21f936acbb89fa5b272efdcf3cf03de58cc (diff) | |
Merge PR#719: Constrexpr.Numeral without bigint
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/3036.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/3036.v b/test-suite/bugs/closed/3036.v index 451bec9b20..3b57310d6e 100644 --- a/test-suite/bugs/closed/3036.v +++ b/test-suite/bugs/closed/3036.v @@ -15,11 +15,11 @@ Definition perm := Qc. Locate Qle_bool. Definition compatibleb (p1 p2 : perm) : bool := -let p1pos := Qle_bool 00 p1 in - let p2pos := Qle_bool 00 p2 in +let p1pos := Qle_bool 0 p1 in + let p2pos := Qle_bool 0 p2 in negb ( (p1pos && p2pos) - || ((p1pos || p2pos) && (negb (Qle_bool 00 ((p1 + p2)%Qc)))))%Qc. + || ((p1pos || p2pos) && (negb (Qle_bool 0 ((p1 + p2)%Qc)))))%Qc. Definition compatible (p1 p2 : perm) := compatibleb p1 p2 = true. |