From f36bf11e994cc269c2ec92b061b082e3516f472f Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 6 May 2022 16:52:48 +0200 Subject: Do not add CompDec on the fly --- unit-tests/Tests_verit_tactics.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'unit-tests/Tests_verit_tactics.v') 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. -- cgit