diff options
| -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. |