diff options
| author | Gaëtan Gilbert | 2019-12-30 12:15:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-15 13:43:24 +0100 |
| commit | f3a6d9dce4d1c291dbaa03bd0e4ed5f33646bff0 (patch) | |
| tree | 5253356704c6db77afc0af218815bbf5b38ffad2 /kernel/indtypes.mli | |
| parent | e4ebe14337743eba09b93c6f5bff1e1d78083741 (diff) | |
generate variance data for section universes (not yet used)
preparation for direct discharge
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 240ba4e2bb..9b54e8b878 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -14,4 +14,5 @@ open Environ open Entries (** Check an inductive. *) -val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body +val check_inductive : env -> sec_univs:Univ.Level.t array option + -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body |