diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2022-05-06 16:52:48 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2022-05-06 16:52:48 +0200 |
| commit | f36bf11e994cc269c2ec92b061b082e3516f472f (patch) | |
| tree | 7db70952d678c5bf4e5283432a42ad58a56761cd /unit-tests | |
| parent | b434a65bb31e18643547ec5861382c61b37c3e7a (diff) | |
| download | smtcoq-f36bf11e994cc269c2ec92b061b082e3516f472f.tar.gz smtcoq-f36bf11e994cc269c2ec92b061b082e3516f472f.zip | |
Do not add CompDec on the fly
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_verit_tactics.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index 4285f96..5164308 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -1562,3 +1562,22 @@ Section TimeoutProp. verit_no_check_timeout 10. Qed. End TimeoutProp. + + +(* Test CompDec open goals *) + +Section OpenCompdec. + + Variable A : Type. + Variable l : list A. + Variable x : A. + Variable H1 : hd_error l = Some x. + Variable H2 : hd_error (@nil A) = None. + Variable H3 : forall x : A, Some x = None -> False. + Variable Hpb : forall x x0 : A, Some x = Some x0 -> x = x0. + + Goal l <> nil. + Proof. verit. Abort. + (* Should leave open CompDec goals but not fail *) + +End OpenCompdec. |