Adding support for lemmas in the command verit

6 files changed, 40 insertions, 2 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
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 8db91fd..06ca01c 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -108,6 +108,12 @@ let pr_constr_env = Printer.pr_constr_env
 
 let lift = Term.lift
 
+let destruct_rel_decl (n, _, t) = n, t
+
+let interp_constr env sigma = Constrintern.interp_constr sigma env
+
+type constr_expr = Topconstr.constr_expr
+                            
 let tclTHEN = Tacticals.tclTHEN
 let tclTHENLAST = Tacticals.tclTHENLAST
 let assert_before = Tactics.assert_tac
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
index ba095c8..7c5edfd 100644
--- a/src/versions/native/structures.mli
+++ b/src/versions/native/structures.mli
@@ -23,6 +23,9 @@ val extern_constr : Term.constr -> Topconstr.constr_expr
 val vernacentries_interp : Topconstr.constr_expr -> unit
 val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds
 val lift : int -> Term.constr -> Term.constr
+val destruct_rel_decl : Term.rel_declaration -> Names.name * Term.constr
+val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> Term.constr
+type constr_expr = Topconstr.constr_expr
 val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
 val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
 val assert_before : Names.name -> Term.types -> Proof_type.tactic
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
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index ec899d8..be63a80 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -135,6 +135,15 @@ let pr_constr_env env = Printer.pr_constr_env env Evd.empty
 
 let lift = Vars.lift
 
+type rel_decl = Context.Rel.Declaration.t
+
+let destruct_rel_decl r = Context.Rel.Declaration.get_name r,
+                          Context.Rel.Declaration.get_type r
+
+type constr_expr = Constrexpr.constr_expr
+                        
+let interp_constr env sigma t = Constrintern.interp_constr env sigma t |> fst
+                        
 let tclTHEN = Tacticals.New.tclTHEN
 let tclTHENLAST = Tacticals.New.tclTHENLAST
 let assert_before = Tactics.assert_before
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
index 86ceb3e..600503d 100644
--- a/src/versions/standard/structures.mli
+++ b/src/versions/standard/structures.mli
@@ -37,6 +37,10 @@ val extern_constr : Term.constr -> Constrexpr.constr_expr
 val vernacentries_interp : Constrexpr.constr_expr -> unit
 val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds
 val lift : int -> Constr.constr -> Constr.constr
+type rel_decl = Context.Rel.Declaration.t                                     
+val destruct_rel_decl : rel_decl -> Names.Name.t * Constr.t
+type constr_expr = Constrexpr.constr_expr
+val interp_constr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Term.constr
 val tclTHEN :
   unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
 val tclTHENLAST :