diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-26 17:01:07 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-26 17:01:07 +0200 |
| commit | 5cb4fb6fbda54976254255ffa5a428f63dee6115 (patch) | |
| tree | 39a548f866d5cf3fbbc750f1b79b2be06baf37f2 /unit-tests/Tests_verit_tactics.v | |
| parent | d90e8b221455dafa32db03f9fdb1601f3127474f (diff) | |
| parent | 3c16cd6919f2f44cf2732e0bcda88b91ddbbbcff (diff) | |
| download | smtcoq-5cb4fb6fbda54976254255ffa5a428f63dee6115.tar.gz smtcoq-5cb4fb6fbda54976254255ffa5a428f63dee6115.zip | |
Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11
Diffstat (limited to 'unit-tests/Tests_verit_tactics.v')
| -rw-r--r-- | unit-tests/Tests_verit_tactics.v | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index a270fdd..73b59f4 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -500,12 +500,21 @@ Qed. Goal forall (i j:int), (i == j) && (negb (i == j)) = false. Proof using. - verit. auto with typeclass_instances. + verit. Qed. +Goal forall (i j:int), + ~ ((i = j) /\ (~ (i = j))). +Proof using. verit. Qed. + Goal forall i j, (i == j) || (negb (i == j)). Proof using. - verit. auto with typeclass_instances. + verit. +Qed. + +Goal forall (i j:int), (i = j) \/ (~ (i = j)). +Proof using. + verit. Qed. @@ -1153,10 +1162,10 @@ Qed. Section AppliedPolymorphicTypes1. Goal forall (f : option Z -> Z) (a b : Z), implb (Z.eqb a b) (Z.eqb (f (Some a)) (f (Some b))). - Proof. verit. auto with typeclass_instances. Qed. + Proof. verit. Qed. Goal forall (f : option Z -> Z) (a b : Z), a = b -> f (Some a) = f (Some b). - Proof. verit. auto with typeclass_instances. Qed. + Proof. verit. Qed. End AppliedPolymorphicTypes1. |