aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--library/declare.ml4
-rw-r--r--library/lib.ml22
-rw-r--r--library/lib.mli5
-rw-r--r--test-suite/bugs/closed/4503.v37
-rw-r--r--test-suite/bugs/closed/HoTT_coq_002.v2
-rw-r--r--test-suite/bugs/closed/HoTT_coq_020.v4
-rw-r--r--theories/Logic/Hurkens.v3
7 files changed, 62 insertions, 15 deletions
diff --git a/library/declare.ml b/library/declare.ml
index 5f6f0fe45..c9d5fdbe2 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -158,7 +158,7 @@ let cache_constant ((sp,kn), obj) =
assert (eq_constant kn' (constant_of_kn kn));
Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
let cst = Global.lookup_constant kn' in
- add_section_constant (cst.const_proj <> None) kn' cst.const_hyps;
+ add_section_constant cst.const_polymorphic kn' cst.const_hyps;
Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
add_constant_kind (constant_of_kn kn) obj.cst_kind
@@ -325,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
let kn' = Global.add_mind dir id mie in
assert (eq_mind kn' (mind_of_kn kn));
let mind = Global.lookup_mind kn' in
- add_section_kn kn' mind.mind_hyps;
+ add_section_kn mind.mind_polymorphic kn' mind.mind_hyps;
Dischargedhypsmap.set_discharged_hyps sp dhyps;
List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
diff --git a/library/lib.ml b/library/lib.ml
index ff8929167..e4617cafb 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -408,17 +408,24 @@ let add_section () =
sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),
(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
+let check_same_poly p vars =
+ let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in
+ if List.exists pred vars then
+ error "Cannot mix universe polymorphic and monomorphic declarations in sections."
+
let add_section_variable id impl poly ctx =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
| (vars,repl,abs)::sl ->
- sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
+ check_same_poly poly vars;
+ sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
let add_section_context ctx =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
| (vars,repl,abs)::sl ->
- sectab := (Context ctx :: vars,repl,abs)::sl
+ check_same_poly true vars;
+ sectab := (Context ctx :: vars,repl,abs)::sl
let extract_hyps (secs,ohyps) =
let rec aux = function
@@ -443,10 +450,11 @@ let instance_from_variable_context sign =
let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx
-let add_section_replacement f g hyps =
+let add_section_replacement f g poly hyps =
match !sectab with
| [] -> ()
| (vars,exps,abs)::sl ->
+ let () = check_same_poly poly vars in
let sechyps,ctx = extract_hyps (vars,hyps) in
let ctx = Univ.ContextSet.to_context ctx in
let subst, ctx = Univ.abstract_universes true ctx in
@@ -454,13 +462,13 @@ let add_section_replacement f g hyps =
sectab := (vars,f (Univ.UContext.instance ctx,args) exps,
g (sechyps,subst,ctx) abs)::sl
-let add_section_kn kn =
+let add_section_kn poly kn =
let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
- add_section_replacement f f
+ add_section_replacement f f poly
-let add_section_constant is_projection kn =
+let add_section_constant poly kn =
let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
- add_section_replacement f f
+ add_section_replacement f f poly
let replacement_context () = pi2 (List.hd !sectab)
diff --git a/library/lib.mli b/library/lib.mli
index 29fc7cd24..513c48549 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -178,9 +178,10 @@ val is_in_section : Globnames.global_reference -> bool
val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit
val add_section_context : Univ.universe_context_set -> unit
-val add_section_constant : bool (* is_projection *) ->
+val add_section_constant : Decl_kinds.polymorphic ->
Names.constant -> Context.named_context -> unit
-val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit
+val add_section_kn : Decl_kinds.polymorphic ->
+ Names.mutual_inductive -> Context.named_context -> unit
val replacement_context : unit -> Opaqueproof.work_list
(** {6 Discharge: decrease the section level if in the current section } *)
diff --git a/test-suite/bugs/closed/4503.v b/test-suite/bugs/closed/4503.v
new file mode 100644
index 000000000..f54d6433d
--- /dev/null
+++ b/test-suite/bugs/closed/4503.v
@@ -0,0 +1,37 @@
+Require Coq.Classes.RelationClasses.
+
+Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
+{ refl : forall x, r x x }.
+
+(* FAILURE 1 *)
+
+Section foo.
+ Polymorphic Universes A.
+ Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
+
+ Fail Definition foo := PO.
+End foo.
+
+
+Module ILogic.
+
+Set Universe Polymorphism.
+
+(* Logical connectives *)
+Class ILogic@{L} (A : Type@{L}) : Type := mkILogic
+{
+ lentails: A -> A -> Prop;
+ lentailsPre:> RelationClasses.PreOrder lentails
+}.
+
+
+End ILogic.
+
+Set Printing Universes.
+
+(* There is stil a problem if the class is universe polymorphic *)
+Section Embed_ILogic_Pre.
+ Polymorphic Universes A T.
+ Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}.
+
+End Embed_ILogic_Pre. \ No newline at end of file
diff --git a/test-suite/bugs/closed/HoTT_coq_002.v b/test-suite/bugs/closed/HoTT_coq_002.v
index ba69f6b15..dba4d5998 100644
--- a/test-suite/bugs/closed/HoTT_coq_002.v
+++ b/test-suite/bugs/closed/HoTT_coq_002.v
@@ -9,7 +9,7 @@ Section SpecializedFunctor.
(* Variable objC : Type. *)
Context `(C : SpecializedCategory objC).
- Polymorphic Record SpecializedFunctor := {
+ Record SpecializedFunctor := {
ObjectOf' : objC -> Type;
ObjectC : Object C
}.
diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v
index 4938b80f9..008fb72c4 100644
--- a/test-suite/bugs/closed/HoTT_coq_020.v
+++ b/test-suite/bugs/closed/HoTT_coq_020.v
@@ -59,8 +59,8 @@ Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C
:= Build_Functor Cat0 C (fun x => match x with end).
Section Law0.
- Variable objC : Type.
- Variable C : Category objC.
+ Polymorphic Variable objC : Type.
+ Polymorphic Variable C : Category objC.
Set Printing All.
Set Printing Universes.
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 8ded74763..841f843c0 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -631,6 +631,8 @@ End NoRetractFromTypeToProp.
Module TypeNeqSmallType.
+Unset Universe Polymorphism.
+
Section Paradox.
(** ** Universe [U] is equal to one of its elements. *)
@@ -655,7 +657,6 @@ Proof.
reflexivity.
Qed.
-
Theorem paradox : False.
Proof.
Generic.paradox p.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 03:53:10 +0000