diff options
Diffstat (limited to 'src/versions/standard/g_smtcoq_standard.ml4')
| -rw-r--r-- | src/versions/standard/g_smtcoq_standard.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4 index 6c3b8cf..2411316 100644 --- a/src/versions/standard/g_smtcoq_standard.ml4 +++ b/src/versions/standard/g_smtcoq_standard.ml4 @@ -109,8 +109,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 |