diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 18:36:55 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 18:36:55 +0200 |
| commit | 6a52af37191e5a6c9b2aa5a91ae3d0d9185ccdd6 (patch) | |
| tree | 8de224f14b73cd34bd81ce18f251ba0cdfe0bb64 /unit-tests | |
| parent | 87ec8048b9da841af7b124b6dc91c9a8550b7585 (diff) | |
| download | smtcoq-6a52af37191e5a6c9b2aa5a91ae3d0d9185ccdd6.tar.gz smtcoq-6a52af37191e5a6c9b2aa5a91ae3d0d9185ccdd6.zip | |
Compatibility with native-coq
Diffstat (limited to 'unit-tests')
| -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 *) |