diff options
| author | Gaëtan Gilbert | 2019-10-05 12:16:34 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-05 12:16:34 +0200 |
| commit | 8398ec48072b0bbe5e571a8d1f1f6c1ace9270f4 (patch) | |
| tree | d13a1039ce27bb947e80eb63781bb64a6037dcef /kernel/section.mli | |
| parent | d7f11221f797e501fe3bcdb06fe7ef3f559869c3 (diff) | |
Remove "is_polymorphic_univ" checks in upper layers.
There were 2:
- when declaring a constraint to avoid monomorphic constraint
referring to polymorphic univs, this check is redundant with the
check in Section.ml
- when declaring a universe context to avoid redeclaring universes,
this is not necessary after recent commits.
Diffstat (limited to 'kernel/section.mli')
| -rw-r--r-- | kernel/section.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/section.mli b/kernel/section.mli index fc3ac141e4..56b4d9ba8f 100644 --- a/kernel/section.mli +++ b/kernel/section.mli @@ -83,5 +83,3 @@ val replacement_context : Environ.env -> 'a t -> Opaqueproof.work_list (** Section segments of all declarations from this section. *) val is_in_section : Environ.env -> GlobRef.t -> 'a t -> bool - -val is_polymorphic_univ : Level.t -> 'a t -> bool |