diff options
Diffstat (limited to 'src/versions/standard/g_smtcoq_standard.ml4')
| -rw-r--r-- | src/versions/standard/g_smtcoq_standard.ml4 | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4 index ab097a1..b8ea279 100644 --- a/src/versions/standard/g_smtcoq_standard.ml4 +++ b/src/versions/standard/g_smtcoq_standard.ml4 @@ -57,6 +57,14 @@ TACTIC EXTEND Tactic_zchaff | [ "zchaff" ] -> [ Zchaff.tactic () ] END +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 := [] ] +END + + TACTIC EXTEND Tactic_verit -| [ "verit" ] -> [ Verit.tactic () ] +| [ "verit_base" constr_list(lpl) ] -> [ Verit.tactic lpl !lemmas_list ] END |