From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 kernel/typeops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1a07bb2fc6..e08f3362db 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -555,7 +555,7 @@ let type_of_projection_constant env (p,u) =
   let cb = lookup_constant cst env in
   match cb.const_proj with
   | Some pb ->
-    if cb.const_polymorphic then
+    if Declareops.constant_is_polymorphic cb then
       Vars.subst_instance_constr u pb.proj_type
     else pb.proj_type
   | None -> raise (Invalid_argument "type_of_projection: not a projection")
-- 
cgit v1.2.3