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 | |
| parent | 6a52af37191e5a6c9b2aa5a91ae3d0d9185ccdd6 (diff) | |
| download | smtcoq-048f0170612ee39f6bc736246fca82d960e79a18.tar.gz smtcoq-048f0170612ee39f6bc736246fca82d960e79a18.zip | |
English comments
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_verit.v | 6 | ||||
| -rw-r--r-- | unit-tests/Tests_zchaff.v | 4 |
2 files changed, 5 insertions, 5 deletions
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index 20523bf..7e356bb 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -411,7 +411,7 @@ End Theorem_Let2. (* verit tactic *) -(* Simple connectors *) +(* Simple connectives *) Goal forall (a:bool), a || negb a. verit. @@ -464,7 +464,7 @@ Goal forall (a:bool), a = a. Qed. -(* Other connectors *) +(* Other connectives *) Goal (false || true) && false = false. Proof. @@ -561,7 +561,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, let a := i == j in 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. |