From 2a07fb44bd453fe9ff2649b498dfb6c0e8001324 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Mar 2021 17:06:22 +0100
Subject: Fix kernel incorrectly assuming the "using" hyps are transitively
 closed

Fix #13903
---
 kernel/term_typing.ml | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3