diff options
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 |