From 048f0170612ee39f6bc736246fca82d960e79a18 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 26 Apr 2016 18:43:02 +0200 Subject: English comments --- unit-tests/Tests_verit.v | 6 +++--- unit-tests/Tests_zchaff.v | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'unit-tests') 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. -- cgit