diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
| commit | f219abfed720305c13875c3c63f9240cf63f78bc (patch) | |
| tree | 69d2c026916128fdb50b8d1c0dbf1be451340d30 /plugins/subtac/subtac_command.mli | |
| parent | 476d60ef0fe0ac015c1e902204cdd7029e10ef0f (diff) | |
| parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) | |
Merge tag 'upstream/8.5_beta1+dfsg'
Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'plugins/subtac/subtac_command.mli')
| -rw-r--r-- | plugins/subtac/subtac_command.mli | 60 |
1 files changed, 0 insertions, 60 deletions
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli deleted file mode 100644 index 72549a01..00000000 --- a/plugins/subtac/subtac_command.mli +++ /dev/null @@ -1,60 +0,0 @@ -open Pretyping -open Evd -open Environ -open Term -open Topconstr -open Names -open Libnames -open Pp -open Vernacexpr -open Constrintern - -val interp_gen : - typing_constraint -> - evar_map ref -> - env -> - ?impls:internalization_env -> - ?allow_patvar:bool -> - ?ltacvars:ltac_sign -> - constr_expr -> constr -val interp_constr : - evar_map ref -> - env -> constr_expr -> constr -val interp_type_evars : - evar_map ref -> - env -> - ?impls:internalization_env -> - constr_expr -> constr -val interp_casted_constr_evars : - evar_map ref -> - env -> - ?impls:internalization_env -> - constr_expr -> types -> constr -val interp_open_constr : - evar_map ref -> env -> constr_expr -> constr -val interp_constr_judgment : - evar_map ref -> - env -> - constr_expr -> unsafe_judgment -val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list - -val interp_binder : Evd.evar_map ref -> - Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr - - -val telescope : - (Names.name * Term.types option * Term.types) list -> - Term.types * (Names.name * Term.types option * Term.types) list * - Term.constr - -val build_wellfounded : - Names.identifier * 'a * Topconstr.local_binder list * - Topconstr.constr_expr * Topconstr.constr_expr -> - Topconstr.constr_expr -> - Topconstr.constr_expr -> 'b -> Subtac_obligations.progress - -val build_recursive : - (fixpoint_expr * decl_notation list) list -> unit - -val build_corecursive : - (cofixpoint_expr * decl_notation list) list -> unit |