diff options
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 |