diff options
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index ab00aa16..ee4148de 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Evd open Environ open Inductiveops @@ -33,6 +32,8 @@ val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> ' val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a +val irrefutable : env -> cases_pattern -> bool + (** {6 Compilation primitive. } *) val compile_cases : @@ -45,11 +46,11 @@ val compile_cases : val constr_of_pat : Environ.env -> Evd.evar_map ref -> - rel_declaration list -> + Context.Rel.Declaration.t list -> Glob_term.cases_pattern -> Names.Id.t list -> Glob_term.cases_pattern * - (rel_declaration list * Term.constr * + (Context.Rel.Declaration.t list * Term.constr * (Term.types * Term.constr list) * Glob_term.cases_pattern) * Names.Id.t list @@ -83,7 +84,7 @@ type tomatch_status = | Pushed of (bool*((constr * tomatch_type) * int list * Name.t)) | Alias of (bool * (Name.t * constr * (constr * types))) | NonDepAlias - | Abstract of int * rel_declaration + | Abstract of int * Context.Rel.Declaration.t type tomatch_stack = tomatch_status list @@ -113,11 +114,11 @@ val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment val prepare_predicate : Loc.t -> (Evarutil.type_constraint -> - Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) -> + Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) -> Environ.env -> Evd.evar_map -> (Term.types * tomatch_type) list -> - Context.rel_context list -> + Context.Rel.t list -> Constr.constr option -> - 'a option -> (Evd.evar_map * Names.name list * Term.constr) list - + glob_constr option -> + (Evd.evar_map * Names.name list * Term.constr) list |