diff options
Diffstat (limited to 'src/versions')
-rw-r--r-- | src/versions/standard/Array/PArray_standard.v | 2 | ||||
-rw-r--r-- | src/versions/standard/Int63/Int63Native_standard.v | 1 | ||||
-rw-r--r-- | src/versions/standard/_CoqProject | 2 | ||||
-rw-r--r-- | src/versions/standard/g_smtcoq_standard.mlg (renamed from src/versions/standard/g_smtcoq_standard.ml4) | 70 |
4 files changed, 39 insertions, 36 deletions
diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v index e116339..ee0dd96 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/versions/standard/Array/PArray_standard.v @@ -14,6 +14,8 @@ trees *) +Declare Scope array_scope. + Require Import Int31. Require Export Int63. Require FMapAVL. diff --git a/src/versions/standard/Int63/Int63Native_standard.v b/src/versions/standard/Int63/Int63Native_standard.v index a5a931b..abb91ee 100644 --- a/src/versions/standard/Int63/Int63Native_standard.v +++ b/src/versions/standard/Int63/Int63Native_standard.v @@ -20,6 +20,7 @@ Definition size := size. Notation int := int31. +Declare Scope int63_scope. Delimit Scope int63_scope with int. Bind Scope int63_scope with int. diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject index e067da8..396a5ba 100644 --- a/src/versions/standard/_CoqProject +++ b/src/versions/standard/_CoqProject @@ -156,5 +156,5 @@ SMT_terms.v State.v Trace.v -g_smtcoq.ml4 +g_smtcoq.mlg smtcoq_plugin.mlpack diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.mlg index bf923cc..8e273db 100644 --- a/src/versions/standard/g_smtcoq_standard.ml4 +++ b/src/versions/standard/g_smtcoq_standard.mlg @@ -12,88 +12,88 @@ DECLARE PLUGIN "smtcoq_plugin" -open Stdarg +{ -(* 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 Stdarg open Ltac_plugin +} + VERNAC COMMAND EXTEND Vernac_zchaff CLASSIFIED AS QUERY | [ "Parse_certif_zchaff" ident(dimacs) ident(trace) string(fdimacs) string(fproof) ] -> - [ + { Zchaff.parse_certif dimacs trace fdimacs fproof - ] + } | [ "Zchaff_Checker" string(fdimacs) string(fproof) ] -> - [ + { Zchaff.checker fdimacs fproof - ] + } | [ "Zchaff_Theorem" ident(name) string(fdimacs) string(fproof) ] -> - [ + { Zchaff.theorem name fdimacs fproof - ] + } END VERNAC COMMAND EXTEND Vernac_verit CLASSIFIED AS QUERY | [ "Parse_certif_verit" ident(t_i) ident(t_func) ident(t_atom) ident(t_form) ident(root) ident(used_roots) ident(trace) string(fsmt) string(fproof) ] -> - [ + { Verit.parse_certif t_i t_func t_atom t_form root used_roots trace fsmt fproof - ] + } | [ "Verit_Checker" string(fsmt) string(fproof) ] -> - [ + { Verit.checker fsmt fproof - ] + } | [ "Verit_Checker_Debug" string(fsmt) string(fproof) ] -> - [ + { Verit.checker_debug fsmt fproof - ] + } | [ "Verit_Theorem" ident(name) string(fsmt) string(fproof) ] -> - [ + { Verit.theorem name fsmt fproof - ] + } END VERNAC COMMAND EXTEND Vernac_lfsc CLASSIFIED AS QUERY | [ "Parse_certif_lfsc" ident(t_i) ident(t_func) ident(t_atom) ident(t_form) ident(root) ident(used_roots) ident(trace) string(fsmt) string(fproof) ] -> - [ + { Lfsc.parse_certif t_i t_func t_atom t_form root used_roots trace fsmt fproof - ] + } | [ "Lfsc_Checker" string(fsmt) string(fproof) ] -> - [ + { Lfsc.checker fsmt fproof - ] + } | [ "Lfsc_Checker_Debug" string(fsmt) string(fproof) ] -> - [ + { Lfsc.checker_debug fsmt fproof - ] + } | [ "Lfsc_Theorem" ident(name) string(fsmt) string(fproof) ] -> - [ + { Lfsc.theorem name fsmt fproof - ] + } END TACTIC EXTEND Tactic_zchaff -| [ "zchaff_bool" ] -> [ Zchaff.tactic () ] -| [ "zchaff_bool_no_check" ] -> [ Zchaff.tactic_no_check () ] +| [ "zchaff_bool" ] -> { Zchaff.tactic () } +| [ "zchaff_bool_no_check" ] -> { Zchaff.tactic_no_check () } END -let lemmas_list = ref [] +{ let lemmas_list = ref [] } VERNAC COMMAND EXTEND Add_lemma CLASSIFIED AS SIDEFF -| [ "Add_lemmas" constr_list(lems) ] -> [ lemmas_list := lems @ !lemmas_list ] -| [ "Clear_lemmas" ] -> [ lemmas_list := [] ] +| [ "Add_lemmas" constr_list(lems) ] -> { lemmas_list := lems @ !lemmas_list } +| [ "Clear_lemmas" ] -> { lemmas_list := [] } END TACTIC EXTEND Tactic_verit -| [ "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 ] +| [ "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 -| [ "cvc4_bool" ] -> [ Lfsc.tactic () ] -| [ "cvc4_bool_no_check" ] -> [ Lfsc.tactic_no_check () ] +| [ "cvc4_bool" ] -> { Lfsc.tactic () } +| [ "cvc4_bool_no_check" ] -> { Lfsc.tactic_no_check () } END |