diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-21 10:00:58 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-21 10:00:58 +0200 |
commit | 13d2c8be2ffb84bc8d40064b223562832e5a5a7e (patch) | |
tree | 8e9b4c8b8c31ee95bcd7eeffaacf72b40215adb3 /src/versions/standard/g_smtcoq_standard.mlg | |
parent | 0955c9b404b2bebbe76a15daaad09c03670e849e (diff) | |
parent | 4a2ef2747950e8a28bfce7ca641bedd7ef71bea1 (diff) | |
download | smtcoq-13d2c8be2ffb84bc8d40064b223562832e5a5a7e.tar.gz smtcoq-13d2c8be2ffb84bc8d40064b223562832e5a5a7e.zip |
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10
Diffstat (limited to 'src/versions/standard/g_smtcoq_standard.mlg')
-rw-r--r-- | src/versions/standard/g_smtcoq_standard.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/versions/standard/g_smtcoq_standard.mlg b/src/versions/standard/g_smtcoq_standard.mlg index 443d558..84ec154 100644 --- a/src/versions/standard/g_smtcoq_standard.mlg +++ b/src/versions/standard/g_smtcoq_standard.mlg @@ -113,8 +113,8 @@ END TACTIC EXTEND Tactic_verit -| [ "verit_bool_base" constr_list(lpl) ] -> { Verit.tactic (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) } -| [ "verit_bool_no_check_base" constr_list(lpl) ] -> { Verit.tactic_no_check (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) } +| [ "verit_bool_base" constr(lpl) ] -> { Verit.tactic lpl (get_lemmas ()) } +| [ "verit_bool_no_check_base" constr(lpl) ] -> { Verit.tactic_no_check lpl (get_lemmas ()) } END TACTIC EXTEND Tactic_cvc4 |