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/declareops.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/declareops.mli')

diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 6c43bffa9e..04a067aff0 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -29,6 +29,7 @@ val constant_has_body : constant_body -> bool
     Only use this function if you know what you're doing. *)
 
 val body_of_constant : constant_body -> Term.constr option
+val type_of_constant : constant_body -> constant_type
 val constraints_of_constant : constant_body -> Univ.constraints
 val universes_of_constant : constant_body -> Univ.universe_context
 
-- 
cgit v1.2.3