diff options
| author | Pierre-Marie Pédrot | 2020-02-07 18:13:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-09 16:38:14 +0100 |
| commit | b6264bb2df9b73b905af126ede49cd31abf0e7da (patch) | |
| tree | 6eddb39c2870eb12be6d6cdb5cfe15f9eaf55513 /kernel/indTyping.mli | |
| parent | 1820f40590ec358b40e3a9c444f80c5283e55292 (diff) | |
Remove the Template Check option.
Diffstat (limited to 'kernel/indTyping.mli')
| -rw-r--r-- | kernel/indTyping.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 8dea8f046d..723ba5459e 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -40,7 +40,6 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option (* Utility function to compute the actual universe parameters of a template polymorphic inductive *) val template_polymorphic_univs : - template_check:bool -> ctor_levels:Univ.LSet.t -> Univ.ContextSet.t -> Constr.rel_context -> |