diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 18:43:02 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 18:43:02 +0200 |
| commit | 048f0170612ee39f6bc736246fca82d960e79a18 (patch) | |
| tree | d0dd2928cbdb657adcf831a95761f7ae79417f2e /unit-tests/Tests_zchaff.v | |
| parent | 6a52af37191e5a6c9b2aa5a91ae3d0d9185ccdd6 (diff) | |
| download | smtcoq-048f0170612ee39f6bc736246fca82d960e79a18.tar.gz smtcoq-048f0170612ee39f6bc736246fca82d960e79a18.zip | |
English comments
Diffstat (limited to 'unit-tests/Tests_zchaff.v')
| -rw-r--r-- | unit-tests/Tests_zchaff.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/unit-tests/Tests_zchaff.v b/unit-tests/Tests_zchaff.v index c452734..8a5077b 100644 --- a/unit-tests/Tests_zchaff.v +++ b/unit-tests/Tests_zchaff.v @@ -148,7 +148,7 @@ Proof. Qed. -(* Le même, mais où a, b et c sont des termes concrets *) +(* The same, but with a, b and c being concrete terms *) Goal forall i j k, ((i == j) || (j == k) || (k == i)) && ((negb (i == j)) || (negb (j == k)) || (negb (k == i))) && ((negb (i == j)) || (j == k)) && ((negb (j == k)) || (k == i)) && ((negb (k == i)) || (i == j)) = false. @@ -184,7 +184,7 @@ Proof. Qed. -(* Other connectors *) +(* Other connectives *) Goal (false || true) && false = false. Proof. |