diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 23:07:38 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 23:07:38 +0200 |
| commit | a5bd782f300c3767936fc3f45df6a09cda185370 (patch) | |
| tree | bb3c0753a54e035fec56f78edbae84485a50b878 /unit-tests | |
| parent | 048f0170612ee39f6bc736246fca82d960e79a18 (diff) | |
| download | smtcoq-a5bd782f300c3767936fc3f45df6a09cda185370.tar.gz smtcoq-a5bd782f300c3767936fc3f45df6a09cda185370.zip | |
Both native-coq and Coq 8.5 are fully supported
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_verit.v | 32 |
1 files changed, 14 insertions, 18 deletions
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index 7e356bb..e63bbaf 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -842,25 +842,21 @@ Proof. verit. Qed. -Section Concrete. - Goal forall (i j:int), +Goal forall (i j:int), (i == j) && (negb (i == j)) = false. - Proof. - verit. - Qed. -End Concrete. - -Section Concrete2. - Lemma concrete2 : forall i j, (i == j) || (negb (i == j)). - Proof. - verit. - Qed. - Check concrete2. -End Concrete2. -Check concrete2. - - -(* Congruence in which some premices are REFL *) +Proof. + verit. + econstructor; eexact Int63Properties.reflect_eqb. +Qed. + +Goal forall i j, (i == j) || (negb (i == j)). +Proof. + verit. + econstructor; eexact Int63Properties.reflect_eqb. +Qed. + + +(* Congruence in which some premises are REFL *) Goal forall (f:Z -> Z -> Z) x y z, implb (Zeq_bool x y) (Zeq_bool (f z x) (f z y)). |