diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 42d1a1f3fc..c7a588d2b4 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -359,7 +359,7 @@ let save_lemma_admitted ~(lemma : t) : unit = let env = Global.env () in let ids_typ = Environ.global_vars_set env typ in let ids_def = Environ.global_vars_set env pproof in - Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) + Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None in let universes = Proof_global.get_initial_euctx lemma.proof in let ctx = UState.check_univ_decl ~poly universes udecl in |