diff options
| -rw-r--r-- | kernel/section.mli | 2 | ||||
| -rw-r--r-- | library/lib.ml | 3 | ||||
| -rw-r--r-- | library/lib.mli | 2 | ||||
| -rw-r--r-- | tactics/declare.ml | 30 |
4 files changed, 5 insertions, 32 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 diff --git a/library/lib.ml b/library/lib.ml index 991e23eb3a..0d9efe2d5d 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -425,9 +425,6 @@ let extract_worklist info = let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env () -let is_polymorphic_univ u = - Section.is_polymorphic_univ u (sections ()) - let replacement_context () = Section.replacement_context (Global.env ()) (sections ()) diff --git a/library/lib.mli b/library/lib.mli index d3315b0f2e..59d77480e9 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -183,8 +183,6 @@ val is_in_section : GlobRef.t -> bool val replacement_context : unit -> Opaqueproof.work_list -val is_polymorphic_univ : Univ.Level.t -> bool - (** {6 Discharge: decrease the section level if in the current section } *) (* XXX Why can't we use the kernel functions ? *) diff --git a/tactics/declare.ml b/tactics/declare.ml index 3ec6f884be..32447f31c1 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -52,11 +52,7 @@ let name_instance inst = let declare_universe_context ~poly ctx = if poly then - (* FIXME: some upper layers declare universes several times, we hack around - by checking whether the universes already exist. *) - let (univs, cstr) = ctx in - let univs = Univ.LSet.filter (fun u -> not (Lib.is_polymorphic_univ u)) univs in - let uctx = Univ.ContextSet.to_context (univs, cstr) in + let uctx = Univ.ContextSet.to_context ctx in let nas = name_instance (Univ.UContext.instance uctx) in Global.push_section_context (nas, uctx) else @@ -606,28 +602,12 @@ let do_universe ~poly l = let do_constraint ~poly l = let open Univ in let u_of_id x = - let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in - Lib.is_polymorphic_univ level, level - in - let in_section = Lib.sections_are_opened () in - let () = - if poly && not in_section then - CErrors.user_err ~hdr:"Constraint" - (str"Cannot declare polymorphic constraints outside sections") - in - let check_poly p p' = - if poly then () - else if p || p' then - CErrors.user_err ~hdr:"Constraint" - (str "Cannot declare a global constraint on " ++ - str "a polymorphic universe, use " - ++ str "Polymorphic Constraint instead") + Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in let constraints = List.fold_left (fun acc (l, d, r) -> - let p, lu = u_of_id l and p', ru = u_of_id r in - check_poly p p'; - Constraint.add (lu, d, ru) acc) - Constraint.empty l + let lu = u_of_id l and ru = u_of_id r in + Constraint.add (lu, d, ru) acc) + Constraint.empty l in let uctx = ContextSet.add_constraints constraints ContextSet.empty in declare_universe_context ~poly uctx |