From 83e0cb59ed9a07bdf0154aaa2169bc94acf88c19 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 27 Mar 2018 02:37:19 +0200 Subject: Swapping Context and Constr: defining declarations on constr in Constr. This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate). --- kernel/typeops.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/typeops.mli') diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 3b2abc777..57acdfe4b 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -28,7 +28,7 @@ val infer_v : env -> constr array -> unsafe_judgment array val infer_type : env -> types -> unsafe_type_judgment val infer_local_decls : - env -> (Id.t * local_entry) list -> (env * Context.Rel.t) + env -> (Id.t * local_entry) list -> (env * Constr.rel_context) (** {6 Basic operations of the typing machine. } *) @@ -102,4 +102,4 @@ val judge_of_case : env -> case_info val type_of_constant_in : env -> pconstant -> types (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit +val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit -- cgit v1.2.3