diff options
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 9f26ae9ce..3df2d6873 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -47,11 +47,11 @@ 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 * constr * + (rel_context * constr * (types * constr list) * Glob_term.cases_pattern) * Names.Id.t list @@ -85,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 @@ -119,6 +119,6 @@ val prepare_predicate : Loc.t -> Environ.env -> Evd.evar_map -> (types * tomatch_type) list -> - Context.Rel.t list -> + rel_context list -> constr option -> 'a option -> (Evd.evar_map * Names.name list * constr) list |