From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 parsing/prettyp.ml | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

(limited to 'parsing/prettyp.ml')

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 4534369f..57028469 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: prettyp.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: prettyp.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
 
 open Pp
 open Util
@@ -246,6 +246,7 @@ let print_safe_judgment env j =
 let print_named_def name body typ =
   let pbody = pr_lconstr body in
   let ptyp = pr_ltype typ in
+  let pbody = if isCast body then surround pbody else pbody in
   (str "*** [" ++ str name ++ str " " ++
      hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
 	      str ":" ++ brk (1,2) ++ ptyp) ++
@@ -278,11 +279,15 @@ let print_constructors envpar names types =
   hv 0 (str "  " ++ pc)
 
 let build_inductive sp tyi =
-  let (mib,mip as specif) = Global.lookup_inductive (sp,tyi) in
+  let (mib,mip) = Global.lookup_inductive (sp,tyi) in
   let params = mib.mind_params_ctxt in
   let args = extended_rel_list 0 params in
   let env = Global.env() in
-  let arity = hnf_prod_applist env (Inductive.type_of_inductive specif) args in
+  let fullarity = match mip.mind_arity with
+    | Monomorphic ar -> ar.mind_user_arity 
+    | Polymorphic ar ->
+	it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt in
+  let arity = hnf_prod_applist env fullarity args in
   let cstrtypes = arities_of_constructors env (sp,tyi) in
   let cstrtypes =
     Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
@@ -325,10 +330,14 @@ let print_body = function
 let print_typed_body (val_0,typ) =
   (print_body val_0 ++ fnl () ++ str "     : " ++ pr_ltype typ ++ fnl ())
 
+let ungeneralized_type_of_constant_type = function
+  | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
+  | NonPolymorphicType t -> t
+
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
   let val_0 = cb.const_body in
-  let typ = cb.const_type in
+  let typ = ungeneralized_type_of_constant_type cb.const_type in
   hov 0 (
     match val_0 with 
     | None -> 
-- 
cgit v1.2.3