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).

---
 printing/prettyp.ml  | 3 ++-
 printing/printer.ml  | 6 +++---
 printing/printmod.ml | 3 ++-
 3 files changed, 7 insertions(+), 5 deletions(-)

(limited to 'printing')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e885f5978..87d7e0980 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -371,7 +371,8 @@ let print_body = function
 let print_typed_body (val_0,typ) =
   (print_body val_0 ++ fnl () ++ str "     : " ++ pr_ltype typ)
 
-let ungeneralized_type_of_constant_type t = t
+let ungeneralized_type_of_constant_type t = 
+  Typeops.type_of_constant_type (Global.env ()) t
 
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
diff --git a/printing/printer.ml b/printing/printer.ml
index 91156e21f..cb10f9661 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -755,16 +755,16 @@ let print_constructors envpar names types =
   hv 0 (str "  " ++ pc)
 
 let build_ind_type env mip =
-  mip.mind_arity.mind_user_arity
+  Inductive.type_of_inductive env mip
 
 let print_one_inductive env mib ((_,i) as ind) =
   let mip = mib.mind_packets.(i) in
   let params = mib.mind_params_ctxt in
   let args = extended_rel_list 0 params in
-  let arity = hnf_prod_applist env (build_ind_type env mip) args in
   let u = if mib.mind_polymorphic then 
       Univ.UContext.instance mib.mind_universes 
     else Univ.Instance.empty in
+  let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
   let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
   let envpar = push_rel_context params env in
@@ -802,7 +802,7 @@ let print_record env mind mib =
   let u = if mib.mind_polymorphic then 
       Univ.UContext.instance mib.mind_universes 
     else Univ.Instance.empty in
-  let arity = hnf_prod_applist env (build_ind_type env mip) args in
+  let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
   let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
   let fields = get_fields cstrtype in
diff --git a/printing/printmod.ml b/printing/printmod.ml
index da5546bac..8d05e2d6d 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -146,7 +146,8 @@ let print_body is_impl env mp (l,body) =
 	  | None -> mt ()
 	  | Some env ->
 	    str " :" ++ spc () ++
-	    hov 0 (Printer.pr_ltype_env env cb.const_type) ++
+	    hov 0 (Printer.pr_ltype_env env 
+		     (Typeops.type_of_constant_type env cb.const_type)) ++
 	    (match cb.const_body with
 	      | Def l when is_impl ->
 		spc () ++
-- 
cgit v1.2.3