diff options
Diffstat (limited to 'vernac/lemmas.ml')
| -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 9ab89c883..dbf7fec66 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -506,7 +506,7 @@ let save_proof ?proof = function 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 (Idset.union ids_typ ids_def)) + Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) | _ -> None in let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in |