diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 20:08:44 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-28 00:39:25 +0200 |
| commit | faaa2848c37444f8f37ac432c25f9f813e1df39b (patch) | |
| tree | 2672d165fd13b5262005406d1496bc6a14e8b521 /src/versions/standard/structures.ml | |
| parent | 7940ef63c654be26b41ce20162207f3c67d0b10a (diff) | |
| download | smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip | |
Adding support for lemmas in the command verit
Diffstat (limited to 'src/versions/standard/structures.ml')
| -rw-r--r-- | src/versions/standard/structures.ml | 9 |
1 files changed, 9 insertions, 0 deletions
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 |