diff options
Diffstat (limited to 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 17 |
1 files changed, 13 insertions, 4 deletions
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 -> |