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