From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: 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. --- pretyping/cases.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'pretyping/cases.mli') 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 -- cgit v1.2.3