diff options
Diffstat (limited to 'src/versions/native/structures.ml')
| -rw-r--r-- | src/versions/native/structures.ml | 6 |
1 files changed, 6 insertions, 0 deletions
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 |