From c71e69a9be2094061e041d60614b090c8381f0b7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 Nov 2017 18:14:38 +0100 Subject: [api] Deprecate all legacy uses of Name.Id in core. This is a first step towards some of the solutions proposed in #6008. --- vernac/lemmas.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/lemmas.ml') 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 -- cgit v1.2.3