From 7002b3daca6da29eadf80019847630b8583c3daf Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 3 Aug 2014 20:02:49 +0200 Subject: Move to a representation of universe polymorphic constants using indices for variables. Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's. Abstraction by variables is handled mostly inside the kernel but could be moved outside. --- pretyping/inductiveops.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index cefd5bd9d..5583eff4d 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -20,7 +20,6 @@ val type_of_inductive : env -> pinductive -> types (** Return type as quoted by the user *) val type_of_constructor : env -> pconstructor -> types -val type_of_constructor_in_ctx : env -> constructor -> types Univ.in_universe_context val type_of_constructors : env -> pinductive -> types array (** Return constructor types in normal form *) -- cgit v1.2.3