aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--library/lib.ml26
-rw-r--r--library/lib.mli2
-rw-r--r--test-suite/bugs/closed/HoTT_coq_020.v2
-rw-r--r--test-suite/bugs/closed/HoTT_coq_098.v2
-rw-r--r--test-suite/bugs/closed/bug_3314.v6
-rw-r--r--test-suite/bugs/closed/bug_4503.v2
-rw-r--r--test-suite/bugs/closed/bug_4816.v5
-rw-r--r--test-suite/success/namedunivs.v1
-rw-r--r--test-suite/success/polymorphism.v9
-rw-r--r--vernac/vernacentries.ml7
10 files changed, 36 insertions, 26 deletions
diff --git a/library/lib.ml b/library/lib.ml
index f19b38cb4f..c4eed7b216 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -436,30 +436,32 @@ type section_data = {
sec_entry : secentry list;
sec_workl : Opaqueproof.work_list;
sec_abstr : abstr_list;
+ sec_poly : bool;
}
-let empty_section_data = {
+let empty_section_data ~poly = {
sec_entry = [];
sec_workl = (Names.Cmap.empty,Names.Mindmap.empty);
sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty);
+ sec_poly = poly;
}
let sectab =
Summary.ref ([] : section_data list) ~name:"section-context"
-let add_section () =
- sectab := empty_section_data :: !sectab
-
-let check_same_poly p vars =
- let pred = function Context _ -> p = false | Variable {poly} -> p != poly in
- if List.exists pred vars then
+let check_same_poly p sec =
+ if p != sec.sec_poly then
user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.")
+let add_section ~poly () =
+ List.iter (fun tab -> check_same_poly poly tab) !sectab;
+ sectab := empty_section_data ~poly :: !sectab
+
let add_section_variable ~name ~kind ~poly univs =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
| s :: sl ->
- List.iter (fun tab -> check_same_poly poly tab.sec_entry) !sectab;
+ List.iter (fun tab -> check_same_poly poly tab) !sectab;
let s = { s with sec_entry = Variable {id=name;kind;poly;univs} :: s.sec_entry } in
sectab := s :: sl
@@ -467,7 +469,7 @@ let add_section_context ctx =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
| s :: sl ->
- check_same_poly true s.sec_entry;
+ check_same_poly true s;
let s = { s with sec_entry = Context ctx :: s.sec_entry } in
sectab := s :: sl
@@ -525,7 +527,7 @@ let add_section_replacement f g poly hyps =
match !sectab with
| [] -> ()
| s :: sl ->
- let () = check_same_poly poly s.sec_entry in
+ let () = check_same_poly poly s in
let sechyps,ctx = extract_hyps (s.sec_entry, hyps) in
let ctx = Univ.ContextSet.to_context ctx in
let inst = Univ.UContext.instance ctx in
@@ -593,7 +595,7 @@ let is_in_section ref =
(*************)
(* Sections. *)
-let open_section id =
+let open_section ~poly id =
let opp = !lib_state.path_prefix in
let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
@@ -604,7 +606,7 @@ let open_section id =
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
lib_state := { !lib_state with path_prefix = prefix };
- add_section ()
+ add_section ~poly ()
(* Restore lib_stk and summaries as before the section opening, and
diff --git a/library/lib.mli b/library/lib.mli
index 01366ddfd0..fe6bf69ec4 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -147,7 +147,7 @@ val library_part : GlobRef.t -> DirPath.t
(** {6 Sections } *)
-val open_section : Id.t -> unit
+val open_section : poly:bool -> Id.t -> unit
val close_section : unit -> unit
(** {6 We can get and set the state of the operations (used in [States]). } *)
diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v
index 73da464bbe..babd180209 100644
--- a/test-suite/bugs/closed/HoTT_coq_020.v
+++ b/test-suite/bugs/closed/HoTT_coq_020.v
@@ -26,6 +26,7 @@ Ltac present_obj from to :=
| [ |- context[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in *
end.
+#[universes(polymorphic)]
Section NaturalTransformationComposition.
Set Universe Polymorphism.
Context `(C : @Category objC).
@@ -58,6 +59,7 @@ Polymorphic Definition Cat0 : Category Empty_set
Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C
:= Build_Functor Cat0 C (fun x => match x with end).
+#[universes(polymorphic)]
Section Law0.
Polymorphic Variable objC : Type.
Polymorphic Variable C : Category objC.
diff --git a/test-suite/bugs/closed/HoTT_coq_098.v b/test-suite/bugs/closed/HoTT_coq_098.v
index bdcd8ba97d..3b58605575 100644
--- a/test-suite/bugs/closed/HoTT_coq_098.v
+++ b/test-suite/bugs/closed/HoTT_coq_098.v
@@ -21,6 +21,7 @@ Polymorphic Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
Admitted.
Module success.
+ #[universes(polymorphic)]
Section SpecializedFunctor.
Set Universe Polymorphism.
Context `(C : @SpecializedCategory objC).
@@ -39,6 +40,7 @@ Module success.
End success.
Module success2.
+ #[universes(polymorphic)]
Section SpecializedFunctor.
Polymorphic Context `(C : @SpecializedCategory objC).
Polymorphic Context `(D : @SpecializedCategory objD).
diff --git a/test-suite/bugs/closed/bug_3314.v b/test-suite/bugs/closed/bug_3314.v
index a5782298c3..794de93b37 100644
--- a/test-suite/bugs/closed/bug_3314.v
+++ b/test-suite/bugs/closed/bug_3314.v
@@ -24,10 +24,10 @@ Fail Eval compute in Lift nat : Prop.
(* = nat
: Prop *)
-Section Hurkens.
+Monomorphic Definition Type2 := Type.
+Monomorphic Definition Type1 := Type : Type2.
- Monomorphic Definition Type2 := Type.
- Monomorphic Definition Type1 := Type : Type2.
+Section Hurkens.
(** Assumption of a retract from Type into Prop *)
diff --git a/test-suite/bugs/closed/bug_4503.v b/test-suite/bugs/closed/bug_4503.v
index 26731e3292..88391c7bb1 100644
--- a/test-suite/bugs/closed/bug_4503.v
+++ b/test-suite/bugs/closed/bug_4503.v
@@ -5,6 +5,7 @@ Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
(* FAILURE 1 *)
+#[universes(polymorphic)]
Section foo.
Polymorphic Universes A.
Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
@@ -30,6 +31,7 @@ End ILogic.
Set Printing Universes.
(* There is still a problem if the class is universe polymorphic *)
+#[universes(polymorphic)]
Section Embed_ILogic_Pre.
Polymorphic Universes A T.
Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}.
diff --git a/test-suite/bugs/closed/bug_4816.v b/test-suite/bugs/closed/bug_4816.v
index 00a523842e..50cb7d280a 100644
--- a/test-suite/bugs/closed/bug_4816.v
+++ b/test-suite/bugs/closed/bug_4816.v
@@ -1,3 +1,4 @@
+#[universes(polymorphic)]
Section foo.
Polymorphic Universes A B.
Fail Constraint A <= B.
@@ -5,12 +6,14 @@ End foo.
(* gives an anomaly Universe undefined *)
Universes X Y.
+#[universes(polymorphic)]
Section Foo.
Polymorphic Universes Z W.
Polymorphic Constraint W < Z.
Fail Definition bla := Type@{W}.
Polymorphic Definition bla := Type@{W}.
+ #[universes(polymorphic)]
Section Bar.
Fail Constraint X <= Z.
End Bar.
@@ -21,8 +24,10 @@ Require Coq.Classes.RelationClasses.
Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
{ refl : forall x, r x x }.
+#[universes(polymorphic)]
Section qux.
Polymorphic Universes A.
+ #[universes(polymorphic)]
Section bar.
Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
End bar.
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v
index f9154ef576..01a2136652 100644
--- a/test-suite/success/namedunivs.v
+++ b/test-suite/success/namedunivs.v
@@ -6,6 +6,7 @@
Unset Strict Universe Declaration.
+#[universes(polymorphic)]
Section lift_strict.
Polymorphic Definition liftlt :=
let t := Type@{i} : Type@{k} in
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 339f798240..9ab8ace39e 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -122,8 +122,6 @@ Fail Definition id1impred := ((forall A : Type1, A) : Type1).
End Hierarchy.
-Section structures.
-
Record hypo : Type := mkhypo {
hypo_type : Type;
hypo_proof : hypo_type
@@ -154,9 +152,6 @@ Polymorphic Definition nest (d : dyn) := {| dyn_proof := d |}.
Polymorphic Definition twoprojs (d : dyn) := dyn_proof d = dyn_proof d.
-End structures.
-
-
Module binders.
Definition mynat@{|} := nat.
@@ -201,7 +196,8 @@ Module binders.
Definition with_mono@{u|u < M} : Type@{M} := Type@{u}.
End binders.
-
+
+#[universes(polymorphic)]
Section cats.
Local Set Universe Polymorphism.
Require Import Utf8.
@@ -307,6 +303,7 @@ Fail Check (let A := Set in fooS (id A)).
Fail Check (let A := Prop in fooS (id A)).
(* Some tests of sort-polymorphisme *)
+#[universes(polymorphic)]
Section S.
Polymorphic Variable A:Type.
(*
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 68b7462bde..e98a15eecc 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -963,9 +963,9 @@ let vernac_include l =
(* Sections *)
-let vernac_begin_section ({v=id} as lid) =
+let vernac_begin_section ~poly ({v=id} as lid) =
Dumpglob.dump_definition lid true "sec";
- Lib.open_section id
+ Lib.open_section ~poly id
let vernac_end_section {CAst.loc} =
Dumpglob.dump_reference ?loc
@@ -2396,8 +2396,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
(* Gallina extensions *)
| VernacBeginSection lid ->
VtNoProof(fun () ->
- unsupported_attributes atts;
- vernac_begin_section lid)
+ vernac_begin_section ~poly:(only_polymorphism atts) lid)
| VernacEndSegment lid ->
VtNoProof(fun () ->
unsupported_attributes atts;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 06:37:01 +0000