From 6a52af37191e5a6c9b2aa5a91ae3d0d9185ccdd6 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 26 Apr 2016 18:36:55 +0200 Subject: Compatibility with native-coq --- unit-tests/Tests_verit.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'unit-tests') 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 *) -- cgit