diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
| commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
| tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /parsing/prettyp.ml | |
| parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) | |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index a22f5796..4534369f 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: prettyp.ml 7938 2006-01-28 22:03:33Z herbelin $ *) +(* $Id: prettyp.ml 8845 2006-05-23 07:41:58Z herbelin $ *) open Pp open Util @@ -278,11 +278,11 @@ let print_constructors envpar names types = hv 0 (str " " ++ pc) let build_inductive sp tyi = - let (mib,mip) = Global.lookup_inductive (sp,tyi) in + let (mib,mip as specif) = 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 mip.mind_user_arity args in + let arity = hnf_prod_applist env (Inductive.type_of_inductive specif) 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 @@ -401,7 +401,7 @@ let print_context with_values = | h::rest when n = None or out_some n > 0 -> (match print_library_entry with_values h with | None -> prec n rest - | Some pp -> prec (option_app ((+) (-1)) n) rest ++ pp ++ fnl ()) + | Some pp -> prec (option_map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () in prec |