diff options
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index d8fad1687..6c2b5bf68 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -10,6 +10,7 @@ open Names open Term open Evd open Environ +open EConstr open Inductiveops open Glob_term open Evarutil @@ -46,12 +47,12 @@ val compile_cases : val constr_of_pat : Environ.env -> Evd.evar_map ref -> - Context.Rel.Declaration.t list -> + rel_context -> Glob_term.cases_pattern -> Names.Id.t list -> Glob_term.cases_pattern * - (Context.Rel.Declaration.t list * Term.constr * - (Term.types * Term.constr list) * Glob_term.cases_pattern) * + (rel_context * constr * + (types * constr list) * Glob_term.cases_pattern) * Names.Id.t list type 'a rhs = @@ -84,7 +85,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 * Context.Rel.Declaration.t + | Abstract of int * rel_declaration type tomatch_stack = tomatch_status list @@ -110,15 +111,14 @@ type 'a pattern_matching_problem = typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } -val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment +val compile : 'a pattern_matching_problem -> unsafe_judgment val prepare_predicate : Loc.t -> (Evarutil.type_constraint -> - Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) -> + Environ.env -> Evd.evar_map ref -> glob_constr -> unsafe_judgment) -> Environ.env -> Evd.evar_map -> - (Term.types * tomatch_type) list -> - Context.Rel.t list -> - Constr.constr option -> - glob_constr option -> - (Evd.evar_map * Names.name list * Term.constr) list + (types * tomatch_type) list -> + rel_context list -> + constr option -> + glob_constr option -> (Evd.evar_map * Names.name list * constr) list |