diff options
Diffstat (limited to 'src/versions/standard/g_smtcoq_standard.ml4')
| -rw-r--r-- | src/versions/standard/g_smtcoq_standard.ml4 | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4 index 2cc4415..bf923cc 100644 --- a/src/versions/standard/g_smtcoq_standard.ml4 +++ b/src/versions/standard/g_smtcoq_standard.ml4 @@ -12,9 +12,12 @@ DECLARE PLUGIN "smtcoq_plugin" -open Genarg open Stdarg -open Constrarg + +(* This is requires since Coq 8.7 because the Ltac machinery became a + plugin + see: https://lists.gforge.inria.fr/pipermail/coq-commits/2017-February/021276.html *) +open Ltac_plugin VERNAC COMMAND EXTEND Vernac_zchaff CLASSIFIED AS QUERY | [ "Parse_certif_zchaff" @@ -86,8 +89,8 @@ END TACTIC EXTEND Tactic_verit -| [ "verit_bool_base" constr_list(lpl) ] -> [ Verit.tactic lpl !lemmas_list ] -| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check lpl !lemmas_list ] +| [ "verit_bool_base" constr_list(lpl) ] -> [ Verit.tactic (List.map EConstr.Unsafe.to_constr lpl) !lemmas_list ] +| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check (List.map EConstr.Unsafe.to_constr lpl) !lemmas_list ] END TACTIC EXTEND Tactic_cvc4 |