From 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 28 Oct 2013 14:08:46 +0100
Subject: Initial work on reintroducing old-style polymorphism for
 compatibility (the stdlib does not compile entirely).

---
 kernel/inductive.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index c4a7452f04..a403003e2f 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -109,6 +109,9 @@ exception SingletonInductiveBecomesProp of Id.t
 
 val max_inductive_sort : sorts array -> universe
 
+val instantiate_universes : env -> rel_context ->
+  template_arity -> constr Lazy.t array -> rel_context * sorts
+
 (** {6 Debug} *)
 
 type size = Large | Strict
-- 
cgit v1.2.3