diff options
Diffstat (limited to 'unit-tests/Tests_verit.v')
| -rw-r--r-- | unit-tests/Tests_verit.v | 6 |
1 files changed, 3 insertions, 3 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 |