Fix #5255: [Context (x : T := y)] should mean [Let x := y].

2 files changed, 40 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/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