summaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_pretyping.mli
blob: 97e56ecb24ab45b464c58407ddb1bfb51a016e07 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
open Term
open Environ
open Names
open Sign
open Evd
open Global
open Topconstr

module Pretyping : Pretyping.S

val subtac_process : env -> evar_defs ref -> identifier -> local_binder list ->
  constr_expr -> constr_expr option -> evar_map * constr * types