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/unification.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/unification.mli') diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 41dcb8ed3..6760283d2 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -82,7 +82,7 @@ val finish_evar_resolution : ?flags:Pretyping.inference_flags -> type 'r abstraction_result = Names.Id.t * named_context_val * - Context.Named.Declaration.t list * Names.Id.t option * + named_declaration list * Names.Id.t option * types * (constr, 'r) Sigma.sigma option val make_abstraction : env -> 'r Sigma.t -> constr -> -- cgit v1.2.3