From bc108fdf6cf42f3ce550f2f258adf7de5fa5bfdc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 12:42:21 +0200
Subject: Introduce an Ind module in the Names API.

This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
---
 library/lib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index 830777003b..d75177aaa9 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -525,7 +525,7 @@ let init () =
 let mp_of_global = let open GlobRef in function
   | VarRef id -> !lib_state.path_prefix.Nametab.obj_mp
   | ConstRef cst -> Names.Constant.modpath cst
-  | IndRef ind -> Names.ind_modpath ind
+  | IndRef ind -> Names.Ind.modpath ind
   | ConstructRef constr -> Names.constr_modpath constr
 
 let rec dp_of_mp = function
-- 
cgit v1.2.3