diff options
| -rw-r--r-- | test-suite/bugs/closed/5255.v | 24 | ||||
| -rw-r--r-- | test-suite/coqchk/univ.v | 13 | ||||
| -rw-r--r-- | toplevel/classes.ml | 18 |
3 files changed, 53 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/5255.v b/test-suite/bugs/closed/5255.v new file mode 100644 index 0000000000..5daaf9edbf --- /dev/null +++ b/test-suite/bugs/closed/5255.v @@ -0,0 +1,24 @@ +Section foo. + Context (x := 1). + Definition foo : x = 1 := eq_refl. +End foo. + +Module Type Foo. + Context (x := 1). + Definition foo : x = 1 := eq_refl. +End Foo. + +Set Universe Polymorphism. + +Inductive unit := tt. +Inductive eq {A} (x y : A) : Type := eq_refl : eq x y. + +Section bar. + Context (x := tt). + Definition bar : eq x tt := eq_refl _ _. +End bar. + +Module Type Bar. + Context (x := tt). + Definition bar : eq x tt := eq_refl _ _. +End Bar. diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v index 84a4009d7e..19eea94b19 100644 --- a/test-suite/coqchk/univ.v +++ b/test-suite/coqchk/univ.v @@ -33,3 +33,16 @@ Inductive finite_of_order T (D : T -> Type) (n : natural) := (rank_injective : injective_in T natural D rank) (rank_onto : forall i, equivalent (less_than i n) (in_image T natural D rank i)). + +(* Constraints *) +Universes i j. +Inductive constraint1 : (Type -> Type) -> Type := mk_constraint1 : constraint1 (fun x : Type@{i} => (x : Type@{j})). +Constraint i < j. +Inductive constraint2 : Type@{j} := mkc2 (_ : Type@{i}). +Universes i' j'. +Constraint i' = j'. +Inductive constraint3 : (Type -> Type) -> Type := mk_constraint3 : constraint3 (fun x : Type@{i'} => (x : Type@{j'})). +Inductive constraint4 : (Type -> Type) -> Type + := mk_constraint4 : let U1 := Type in + let U2 := Type in + constraint4 (fun x : U1 => (x : U2)). diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 8142d48d88..d3da263dde 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -383,7 +383,13 @@ let context poly l = let ctx = Univ.ContextSet.to_context !uctx in (* Declare the universe context once *) let () = uctx := Univ.ContextSet.empty in - let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in + let decl = match b with + | None -> + (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) + | Some b -> + let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in + (DefinitionEntry entry, IsAssumption Logical) + in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in match class_of_constr t with | Some (rels, ((tc,_), args) as _cl) -> @@ -399,9 +405,17 @@ let context poly l = in let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in - let nstatus = + let nstatus = match b with + | None -> pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl Vernacexpr.NoInline (Loc.ghost, id)) + | Some b -> + let ctx = Univ.ContextSet.to_context !uctx in + let decl = (Discharge, poly, Definition) in + let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in + let hook = Lemmas.mk_hook (fun _ gr -> gr) in + let _ = Command.declare_definition id decl entry [] [] hook in + Lib.sections_are_opened () || Lib.is_modtype_strict () in let () = uctx := Univ.ContextSet.empty in status && nstatus |