From 23fc1c59d78ffb524265caa1908503f50816335a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 6 Oct 2018 11:04:03 +0200
Subject: A state-free version of is_polymorphic.

---
 library/global.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index 53a72a4e49..769a4bea38 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -227,13 +227,7 @@ let universes_of_global env r =
 let universes_of_global gr = 
   universes_of_global (env ()) gr
 
-let is_polymorphic r =
-  let env = env() in 
-  match r with
-  | VarRef id -> false
-  | ConstRef c -> Environ.polymorphic_constant c env
-  | IndRef ind -> Environ.polymorphic_ind ind env
-  | ConstructRef cstr -> Environ.polymorphic_ind (inductive_of_constructor cstr) env
+let is_polymorphic r = Environ.is_polymorphic (env()) r
 
 let is_template_polymorphic r = 
   let env = env() in 
-- 
cgit v1.2.3