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.

---
 kernel/inductive.mli | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 8bd1a56058..9140d171d0 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -35,14 +35,12 @@ val lookup_mind_specif : env -> inductive -> mind_specif
 (** {6 Functions to build standard types related to inductive } *)
 val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list
 
-val make_inductive_subst : mutual_inductive_body -> universe_instance -> universe_level_subst
-
 val inductive_instance : mutual_inductive_body -> universe_instance
 val inductive_context : mutual_inductive_body -> universe_context
 val inductive_paramdecls : mutual_inductive_body puniverses -> rel_context
 
 val instantiate_inductive_constraints : 
-  mutual_inductive_body -> universe_level_subst -> constraints
+  mutual_inductive_body -> universe_instance -> constraints
 
 val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained
 val constrained_type_of_inductive_knowing_parameters : 
@@ -59,7 +57,6 @@ val elim_sorts : mind_specif -> sorts_family list
 
 val constrained_type_of_constructor : pconstructor -> mind_specif -> types constrained
 val type_of_constructor : pconstructor -> mind_specif -> types
-val type_of_constructor_in_ctx : constructor -> mind_specif -> types in_universe_context
 
 (** Return constructor types in normal form *)
 val arities_of_constructors : pinductive -> mind_specif -> types array
-- 
cgit v1.2.3