blob: afe554c87e66a000d4337e6f7d3a3ebc826545d1 (
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 -> Subtac_obligations.progress
|
