Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.

1 files changed, 7 insertions, 7 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f93b24b3e..e28c8e826 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -385,10 +385,10 @@ let build_constant_declaration kn env result =
     let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
     if not (Id.Set.subset inferred_set declared_set) then
-      let l = Id.Set.elements (Idset.diff inferred_set declared_set) in
+      let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in
       let n = List.length l in
-      let declared_vars = Pp.pr_sequence Id.print (Idset.elements declared_set) in
-      let inferred_vars = Pp.pr_sequence Id.print (Idset.elements inferred_set) in
+      let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in
+      let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in
       let missing_vars  = Pp.pr_sequence Id.print (List.rev l) in
       user_err Pp.(prlist str
          ["The following section "; (String.plural n "variable"); " ";
@@ -414,7 +414,7 @@ let build_constant_declaration kn env result =
            we must look at the body NOW, if any *)
         let ids_typ = global_vars_set env typ in
         let ids_def = match def with
-        | Undef _ -> Idset.empty
+        | Undef _ -> Id.Set.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
         | OpaqueDef lc ->
             let vars =
@@ -425,7 +425,7 @@ let build_constant_declaration kn env result =
             if !Flags.record_aux_file then record_aux env ids_typ vars;
             vars
         in
-        keep_hyps env (Idset.union ids_typ ids_def), def
+        keep_hyps env (Id.Set.union ids_typ ids_def), def
     | None ->
         if !Flags.record_aux_file then
           record_aux env Id.Set.empty Id.Set.empty;
@@ -438,14 +438,14 @@ let build_constant_declaration kn env result =
         | Def cs as x ->
             let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
-            let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
+            let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
             OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
               let ids_typ = global_vars_set env typ in
               let ids_def = global_vars_set env c in
-              let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
+              let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
               check declared inferred) lc) in
   let univs = result.cook_universes in
   let tps =