diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-10-28 14:08:46 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:54 +0200 |
| commit | 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 (patch) | |
| tree | 9e83ae395173699a7c5b6f00648c4336bedb7afd /printing | |
| parent | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff) | |
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 3 | ||||
| -rw-r--r-- | printing/printer.ml | 6 | ||||
| -rw-r--r-- | printing/printmod.ml | 3 |
3 files changed, 7 insertions, 5 deletions
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 () ++ |