diff options
| -rw-r--r-- | engine/univNames.ml | 15 | ||||
| -rw-r--r-- | engine/univNames.mli | 7 | ||||
| -rw-r--r-- | engine/universes.ml | 4 | ||||
| -rw-r--r-- | engine/universes.mli | 6 | ||||
| -rw-r--r-- | interp/declare.ml | 3 | ||||
| -rw-r--r-- | library/lib.ml | 15 | ||||
| -rw-r--r-- | library/lib.mli | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/8478.v | 11 |
8 files changed, 29 insertions, 34 deletions
diff --git a/engine/univNames.ml b/engine/univNames.ml index 9e4c6e47fc..70cdd3a2db 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -11,7 +11,6 @@ open Util open Names open Univ -open Nametab let qualid_of_level l = @@ -31,20 +30,6 @@ let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l) (** Global universe information outside the kernel, to handle polymorphic universe names in sections that have to be discharged. *) -let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref) - -let add_global_universe u p = - match Level.name u with - | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map - | None -> () - -let is_polymorphic l = - match Level.name l with - | Some n -> - (try Nametab.UnivIdMap.find n !universe_map - with Not_found -> false) - | None -> false - (** Local universe names of polymorphic references *) type universe_binders = Univ.Level.t Names.Id.Map.t diff --git a/engine/univNames.mli b/engine/univNames.mli index d794d7b744..bd4062ade4 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -13,13 +13,6 @@ open Univ val pr_with_global_universes : Level.t -> Pp.t val qualid_of_level : Level.t -> Libnames.qualid -(** Global universe information outside the kernel, to handle - polymorphic universes in sections that have to be discharged. *) -val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit - -(** Is [lvl] a global polymorphic universe? (ie section polymorphic universe) *) -val is_polymorphic : Level.t -> bool - (** Local universe name <-> level mapping *) type universe_binders = Univ.Level.t Names.Id.Map.t diff --git a/engine/universes.ml b/engine/universes.ml index c7e5f654a1..5d0157b2db 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -19,10 +19,6 @@ type univ_name_list = UnivNames.univ_name_list let pr_with_global_universes = UnivNames.pr_with_global_universes let reference_of_level = UnivNames.qualid_of_level -let add_global_universe = UnivNames.add_global_universe - -let is_polymorphic = UnivNames.is_polymorphic - let empty_binders = UnivNames.empty_binders let register_universe_binders = UnivNames.register_universe_binders diff --git a/engine/universes.mli b/engine/universes.mli index 7ca33f47a1..0d3bae4c95 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -25,12 +25,6 @@ val pr_with_global_universes : Level.t -> Pp.t val reference_of_level : Level.t -> Libnames.qualid [@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"] -val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit -[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"] - -val is_polymorphic : Level.t -> bool -[@@ocaml.deprecated "Use [UnivNames.is_polymorphic]"] - type universe_binders = UnivNames.universe_binders [@@ocaml.deprecated "Use [UnivNames.universe_binders]"] diff --git a/interp/declare.ml b/interp/declare.ml index 22e6cf9d1c..23c68b5e18 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -491,7 +491,6 @@ let add_universe src (dp, i) = Option.iter (fun poly -> let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in Global.push_context_set poly ctx; - UnivNames.add_global_universe level poly; if poly then Lib.add_section_context ctx) optpoly @@ -580,7 +579,7 @@ 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 - UnivNames.is_polymorphic level, level + Lib.is_polymorphic_univ level, level in let in_section = Lib.sections_are_opened () in let () = diff --git a/library/lib.ml b/library/lib.ml index 8ebe44890c..07026a9c2a 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -440,6 +440,21 @@ let add_section_context ctx = check_same_poly true vars; sectab := (Context ctx :: vars,repl,abs)::sl +exception PolyFound of bool (* make this a let exception once possible *) +let is_polymorphic_univ u = + try + let open Univ in + List.iter (fun (vars,_,_) -> + List.iter (function + | Variable (_,_,poly,(univs,_)) -> + if LSet.mem u univs then raise (PolyFound poly) + | Context (univs,_) -> + if LSet.mem u univs then raise (PolyFound true) + ) vars + ) !sectab; + false + with PolyFound b -> b + let extract_hyps (secs,ohyps) = let rec aux = function | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> diff --git a/library/lib.mli b/library/lib.mli index 9933b762ba..a7d21060e9 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -183,6 +183,8 @@ val add_section_kn : Decl_kinds.polymorphic -> MutInd.t -> Constr.named_context -> unit 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 } *) val discharge_kn : MutInd.t -> MutInd.t diff --git a/test-suite/bugs/closed/8478.v b/test-suite/bugs/closed/8478.v new file mode 100644 index 0000000000..8baaf8686a --- /dev/null +++ b/test-suite/bugs/closed/8478.v @@ -0,0 +1,11 @@ +Set Universe Polymorphism. +Set Printing Universes. +Unset Strict Universe Declaration. + +Monomorphic Universe v. + +Section Foo. + Let bar := Type@{u}. + Fail Monomorphic Constraint bar.u < v. + +End Foo. (* was anomaly undeclared universe due to the constraint *) |