diff options
| -rw-r--r-- | kernel/term_typing.ml | 18 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13903.v | 5 |
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. |