diff options
Diffstat (limited to 'pretyping/cases.mli')
-rw-r--r-- | pretyping/cases.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index ab00aa165..ba566f374 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 @@ -117,7 +118,6 @@ val prepare_predicate : Loc.t -> 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 - |