diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-26 16:18:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:44 +0100 |
| commit | b4b90c5d2e8c413e1981c456c933f35679386f09 (patch) | |
| tree | fc84ec244390beb2f495b024620af2e130ad5852 /pretyping/cases.mli | |
| parent | 78a8d59b39dfcb07b94721fdcfd9241d404905d2 (diff) | |
Definining EConstr-based contexts.
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
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 |