blob: b62a8766aa9a75786c59ef7dc6a14f8705a625b8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
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
val subtac_proof : env -> evar_defs ref -> identifier -> local_binder list ->
constr_expr -> constr_expr option -> unit
|
