diff options
Diffstat (limited to 'src/versions/native/smtcoq_plugin_native.ml4')
| -rw-r--r-- | src/versions/native/smtcoq_plugin_native.ml4 | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/versions/native/smtcoq_plugin_native.ml4 b/src/versions/native/smtcoq_plugin_native.ml4 index da0671e..f3c571c 100644 --- a/src/versions/native/smtcoq_plugin_native.ml4 +++ b/src/versions/native/smtcoq_plugin_native.ml4 @@ -58,6 +58,14 @@ TACTIC EXTEND Tactic_zchaff | [ "zchaff" ] -> [ Zchaff.tactic () ] END +let lemmas_list = ref [] + +VERNAC COMMAND EXTEND Add_lemma +| [ "Add_lemmas" constr_list(lems) ] -> [ lemmas_list := lems @ !lemmas_list ] +| [ "Clear_lemmas" ] -> [ lemmas_list := [] ] +END + + TACTIC EXTEND Tactic_verit -| [ "verit" ] -> [ Verit.tactic () ] +| [ "verit_base" constr_list(lpl) ] -> [ Verit.tactic lpl !lemmas_list ] END |