diff options
| author | Pierre-Marie Pédrot | 2019-12-18 16:52:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-18 16:52:10 +0100 |
| commit | dfdfa9eeedebb0aec2cd72be9c1eee27ca9b2fab (patch) | |
| tree | c6e4c772dae91a047c488f20fb3b03afd384300a /kernel/inferCumulativity.mli | |
| parent | 6b9f6c365ec5b478e79f70cf2a1ae4faed809b74 (diff) | |
| parent | 467d4f28802bf07bb0cdb748c78f0936219ceb8d (diff) | |
Merge PR #11027: Cleanup post #10647 (expose comind universe handling)
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/inferCumulativity.mli')
| -rw-r--r-- | kernel/inferCumulativity.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli index a234e334d1..2bddfe21e2 100644 --- a/kernel/inferCumulativity.mli +++ b/kernel/inferCumulativity.mli @@ -9,6 +9,4 @@ (************************************************************************) val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> - Entries.mutual_inductive_entry - -val dummy_variance : Entries.universes_entry -> Univ.Variance.t array + Univ.Variance.t array option |