From 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Mon, 28 Oct 2013 14:08:46 +0100
Subject: Initial work on reintroducing old-style polymorphism for
 compatibility (the stdlib does not compile entirely).

---
 library/assumptions.ml |  2 +-
 library/declare.ml     |  3 ++-
 library/global.ml      | 18 ++++++++++++------
 library/impargs.ml     |  2 +-
 library/universes.ml   | 14 +++++++++-----
 5 files changed, 25 insertions(+), 14 deletions(-)

(limited to 'library')

diff --git a/library/assumptions.ml b/library/assumptions.ml
index 9cfe531ce..37585caa4 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -222,7 +222,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) =
   and add_kn kn s acc =
     let cb = lookup_constant kn in
     let do_type cst =
-      let ctype = cb.Declarations.const_type in
+      let ctype = Global.type_of_global_unsafe (Globnames.ConstRef kn) in
 	(s,ContextObjectMap.add cst ctype acc)
     in
     let (s,acc) =
diff --git a/library/declare.ml b/library/declare.ml
index 820e72369..45015ac65 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -222,7 +222,8 @@ let declare_sideff se =
   in
   let ty_of cb =
     match cb.Declarations.const_type with
-    | (* Declarations.NonPolymorphicType  *)t -> Some t in
+    | Declarations.RegularArity t -> Some t 
+    | Declarations.TemplateArity _ -> None in
   let cst_of cb =
     let pt, opaque = pt_opaque_of cb in
     let ty = ty_of cb in
diff --git a/library/global.ml b/library/global.ml
index 16b07db25..fbba81b51 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -151,10 +151,16 @@ let type_of_global_unsafe r =
   match r with
   | VarRef id -> Environ.named_type id env
   | ConstRef c -> 
-     let cb = Environ.lookup_constant c env in cb.Declarations.const_type
+     let cb = Environ.lookup_constant c env in 
+       Typeops.type_of_constant_type env cb.Declarations.const_type
   | IndRef ind ->
-     let (mib, oib) = Inductive.lookup_mind_specif env ind in
-       oib.Declarations.mind_arity.Declarations.mind_user_arity
+     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
+     let inst = 
+       if mib.Declarations.mind_polymorphic then 
+	 Univ.UContext.instance mib.Declarations.mind_universes
+       else Univ.Instance.empty
+     in
+       Inductive.type_of_inductive env (specif, inst)
   | ConstructRef cstr ->
      let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
      let inst = Univ.UContext.instance mib.Declarations.mind_universes in
@@ -169,13 +175,13 @@ let type_of_global_in_context env r =
      let univs = 
        if cb.const_polymorphic then Future.force cb.const_universes 
        else Univ.UContext.empty
-     in cb.Declarations.const_type, univs
+     in Typeops.type_of_constant_type env cb.Declarations.const_type, univs
   | IndRef ind ->
-     let (mib, oib) = Inductive.lookup_mind_specif env ind in
+     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
      let univs = 
        if mib.mind_polymorphic then mib.mind_universes 
        else Univ.UContext.empty
-     in oib.Declarations.mind_arity.Declarations.mind_user_arity, univs
+     in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs
   | ConstructRef cstr ->
      let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
      let univs = 
diff --git a/library/impargs.ml b/library/impargs.ml
index 5a44b5bdb..f0292762f 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -403,7 +403,7 @@ let compute_semi_auto_implicits env f manual t =
 let compute_constant_implicits flags manual cst =
   let env = Global.env () in
   let cb = Environ.lookup_constant cst env in
-  let ty = cb.const_type in
+  let ty = Typeops.type_of_constant_type env cb.const_type in
   let impls = compute_semi_auto_implicits env flags manual ty in
     impls
     (* match cb.const_proj with *)
diff --git a/library/universes.ml b/library/universes.ml
index c7009b400..73a0b2b1c 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -144,17 +144,21 @@ let type_of_reference env r =
   | VarRef id -> Environ.named_type id env, ContextSet.empty
   | ConstRef c ->
      let cb = Environ.lookup_constant c env in
+     let ty = Typeops.type_of_constant_type env cb.const_type in
        if cb.const_polymorphic then
 	 let (inst, subst), ctx = fresh_instance_from (Future.force cb.const_universes) in
-	   Vars.subst_univs_constr subst cb.const_type, ctx
-       else cb.const_type, ContextSet.empty
+	   Vars.subst_univs_constr subst ty, ctx
+       else ty, ContextSet.empty
 
   | IndRef ind ->
-     let (mib, oib) = Inductive.lookup_mind_specif env ind in
+     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
        if mib.mind_polymorphic then
 	 let (inst, subst), ctx = fresh_instance_from mib.mind_universes in
-	   Vars.subst_univs_constr subst oib.mind_arity.mind_user_arity, ctx
-       else oib.mind_arity.mind_user_arity, ContextSet.empty
+	 let ty = Inductive.type_of_inductive env (specif, inst) in
+	   ty, ctx
+       else
+	 let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
+	   ty, ContextSet.empty
   | ConstructRef cstr ->
      let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
        if mib.mind_polymorphic then
-- 
cgit v1.2.3