diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2022-04-14 18:09:46 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2022-04-14 18:09:46 +0200 |
commit | d2585fac6defa17889a0244556b6822fc0c3cb4e (patch) | |
tree | ca0f10fb4be4caadc348670b0fde3ddd49d19cd9 /unit-tests | |
parent | 7ce6bf4f7740de4c69877ec9179520bcaa0d014c (diff) | |
parent | 1f21e1f95d43f5e76e38e1737de9a2a0322fd71c (diff) | |
download | smtcoq-d2585fac6defa17889a0244556b6822fc0c3cb4e.tar.gz smtcoq-d2585fac6defa17889a0244556b6822fc0c3cb4e.zip |
Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13
Diffstat (limited to 'unit-tests')
-rw-r--r-- | unit-tests/Tests_verit_tactics.v | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index a6ea27b..4285f96 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -1498,3 +1498,67 @@ Section OCamlCompDec. x ++ y = a0::nil -> x = nil /\ y = a0::nil \/ x = a0::nil /\ y = nil. Proof. verit_no_check. Qed. End OCamlCompDec. + + +Section TimeoutBool. + Variable P : Z -> bool. + Variable H0 : P 0. + Variable HInd : forall n, implb (P n) (P (n + 1)). + + Goal P 3. + Proof. + verit_bool_base_auto_timeout (Some (H0, HInd)) 10. + Qed. + + Goal P 3. + Proof. + verit_bool_no_check_base_auto_timeout (Some (H0, HInd)) 10. + Qed. + + Goal P 3. + Proof. + verit_bool_timeout (H0, HInd) 10. + Qed. + + Goal P 3. + Proof. + verit_bool_timeout 10. + Qed. + + Goal P 3. + Proof. + verit_bool_no_check_timeout (H0, HInd) 10. + Qed. + + Goal P 3. + Proof. + verit_bool_no_check_timeout 10. + Qed. +End TimeoutBool. + + +Section TimeoutProp. + Variable P : Z -> bool. + Variable H0 : P 0. + Variable HInd : forall n, (P n) -> (P (n + 1)). + + Goal P 3. + Proof. + verit_timeout (H0, HInd) 10. + Qed. + + Goal P 3. + Proof. + verit_timeout 10. + Qed. + + Goal P 3. + Proof. + verit_no_check_timeout (H0, HInd) 10. + Qed. + + Goal P 3. + Proof. + verit_no_check_timeout 10. + Qed. +End TimeoutProp. |