diff options
| author | Gaëtan Gilbert | 2020-03-10 14:19:30 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-10 14:19:30 +0100 |
| commit | cffb0ed6f58188b8ea01d54a5349d28313b86dc1 (patch) | |
| tree | 21c770ded4937e00419947f4ae31840217ce4978 /kernel/inductive.mli | |
| parent | f1188b9a3f32eef7657bb46026447718f6fb6055 (diff) | |
| parent | 74df1a17d7d58d4fa99de58899e08de5bbe97810 (diff) | |
Merge PR #11764: Simplify mutual template polymorphism
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index b690fe1157..90571844b9 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -123,9 +123,6 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : Sorts.t array -> Universe.t -val instantiate_universes : Constr.rel_context -> - template_arity -> param_univs -> Constr.rel_context * Sorts.t - (** {6 Debug} *) type size = Large | Strict |