diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-10-28 14:08:46 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:54 +0200 |
| commit | 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 (patch) | |
| tree | 9e83ae395173699a7c5b6f00648c4336bedb7afd /kernel/inductive.mli | |
| parent | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff) | |
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index c4a7452f0..a403003e2 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 |