From 1ed00e4f8cded2a2024b66c3f7f4deee6ecd7c83 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Fri, 8 Nov 2013 11:31:22 +0100
Subject: - Fix bug preventing apply from unfolding Fixpoints. - Remove
 Universe Polymorphism flags everywhere. - Properly infer, discharge template
 arities and fix substitution inside them (kernel code to check for
 correctness). - Fix tactics that were supposing universe polymorphic
 constants/inductives to be parametric on that status. Required to make
 interp_constr* return the whole evar universe context now. - Fix the
 univ/level/instance hashconsing to respect the fact that marshalling doesn't
 preserve sharing, sadly losing most of its benefits. Short-term solution is
 to add hashes to these for faster comparison, longer term requires rewriting
 all serialization code.

Conflicts:
	kernel/univ.ml
	tactics/tactics.ml
	theories/Logic/EqdepFacts.v
---
 library/global.ml | 36 ++++++++++++++++++++++++++++--------
 1 file changed, 28 insertions(+), 8 deletions(-)

(limited to 'library/global.ml')

diff --git a/library/global.ml b/library/global.ml
index 74a2a1c0e..6c088e542 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -189,18 +189,38 @@ let type_of_global_in_context env r =
      let inst = Univ.UContext.instance univs in
        Inductive.type_of_constructor (cstr,inst) specif, univs
 
+let universes_of_global env r = 
+  let open Declarations in
+    match r with
+    | VarRef id -> Univ.UContext.empty
+    | ConstRef c -> 
+      let cb = Environ.lookup_constant c env in 
+	Declareops.universes_of_constant cb
+    | IndRef ind ->
+      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
+	mib.mind_universes 
+    | ConstructRef cstr ->
+      let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+	mib.mind_universes 
+
+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 -> 
-     let cb = Environ.lookup_constant c env in cb.Declarations.const_polymorphic
-  | IndRef ind ->
-     let (mib, oib) = Inductive.lookup_mind_specif env ind in
-       mib.Declarations.mind_polymorphic
-  | ConstructRef cstr ->
-     let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-       mib.Declarations.mind_polymorphic
+  | 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_template_polymorphic r = 
+  let env = env() in 
+  match r with
+  | VarRef id -> false
+  | ConstRef c -> Environ.template_polymorphic_constant c env
+  | IndRef ind -> Environ.template_polymorphic_ind ind env
+  | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env
 
 let current_dirpath () = 
   Safe_typing.current_dirpath (safe_env ())
-- 
cgit v1.2.3