blob: ba0b7cd23b6d4d7496f97e79b5f1c2fd628afdab (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
open Term
open Environ
open Names
open Sign
open Evd
open Global
open Topconstr
open Implicit_quantifiers
open Impargs
module Pretyping : Pretyping.S
val interp :
Environ.env ->
Evd.evar_defs ref ->
Rawterm.rawconstr ->
Evarutil.type_constraint -> Term.constr * Term.constr
val subtac_process : env -> evar_defs ref -> identifier -> local_binder list ->
constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list
val subtac_proof : Decl_kinds.definition_kind -> Tacexpr.declaration_hook ->
env -> evar_defs ref -> identifier -> local_binder list ->
constr_expr -> constr_expr option -> Subtac_obligations.progress
|
