From aa3d78fefde6897a50273c83f944b6617963a9bc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 13:58:13 +0200
Subject: Similar introduction of a Construct module in the Names API.

---
 library/lib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/lib.ml b/library/lib.ml
index d75177aaa9..fa0a95d366 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -526,7 +526,7 @@ 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
-  | ConstructRef constr -> Names.constr_modpath constr
+  | ConstructRef constr -> Names.Construct.modpath constr
 
 let rec dp_of_mp = function
   |Names.MPfile dp -> dp
-- 
cgit v1.2.3