diff options
| author | Pierre-Marie Pédrot | 2019-10-13 16:03:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-13 16:03:43 +0200 |
| commit | 564f265bfda10a2c6d4e7297dec47a14ad4b61b3 (patch) | |
| tree | 17ceaf5d055c0c2a8eb02ccb364d832f5ef694a7 /kernel/section.mli | |
| parent | cc4cddda2eb2a05f685c8404e4864ea0bcdac6eb (diff) | |
| parent | 8398ec48072b0bbe5e571a8d1f1f6c1ace9270f4 (diff) | |
Merge PR #10670: ComAssumption cleanup
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
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 |