diff options
Diffstat (limited to 'unit-tests/Tests_verit.v')
| -rw-r--r-- | unit-tests/Tests_verit.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index 53cb9fb..20523bf 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -842,22 +842,22 @@ Proof. verit. Qed. -Section Concret. - Goal forall i j, +Section Concrete. + Goal forall (i j:int), (i == j) && (negb (i == j)) = false. Proof. verit. Qed. -End Concret. +End Concrete. -Section Concret2. - Lemma concret : forall i j, (i == j) || (negb (i == j)). +Section Concrete2. + Lemma concrete2 : forall i j, (i == j) || (negb (i == j)). Proof. verit. Qed. - Check concret. -End Concret2. -Check concret. + Check concrete2. +End Concrete2. +Check concrete2. (* Congruence in which some premices are REFL *) |