Fix kernel incorrectly assuming the "using" hyps are transitively closed

Fix #13903

2 files changed, 13 insertions, 10 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 24aa4ed771..013892ad74 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -269,16 +269,14 @@ let build_constant_declaration env result =
         in
         Environ.really_needed env (Id.Set.union ids_typ ids_def), def
     | Some declared ->
-      let needed = Environ.really_needed env declared in
-      (* Transitive closure ensured by the upper layers *)
-      let () = assert (Id.Set.equal needed declared) in
-        (* We use the declared set and chain a check of correctness *)
-        declared,
-        match def with
-        | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *)
-        | Def cs as x ->
-          let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in
-          x
+      let declared = Environ.really_needed env declared in
+      (* We use the declared set and chain a check of correctness *)
+      declared,
+      match def with
+      | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *)
+      | Def cs as x ->
+        let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in
+        x
   in
   let univs = result.cook_universes in
   let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
diff --git a/test-suite/bugs/closed/bug_13903.v b/test-suite/bugs/closed/bug_13903.v
new file mode 100644
index 0000000000..7c1820b85c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13903.v
@@ -0,0 +1,5 @@
+Section test.
+Variables (T : Type) (x : T).
+#[using="x"] Definition test : unit := tt.
+End test.
+Check test : forall T, T -> unit.