diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-28 09:58:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-28 09:58:16 +0000 |
| commit | c09da18298d947335cb572ca5f688298b1b8238e (patch) | |
| tree | e4c14c5daf47027928996a4390bcce55b28f0f50 /parsing | |
| parent | 3f41c704aa09301df18cfc90f72a3895e169d74c (diff) | |
Ajout option Set Printing Universes et amélioration affichage des univers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9304 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/ppconstr.ml | 4 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 10 |
2 files changed, 10 insertions, 4 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index a003c1405..e1f375d0a 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -113,12 +113,14 @@ let pr_optc pr = function | None -> mt () | Some x -> pr_sep_com spc pr x +let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" + let pr_universe = Univ.pr_uni let pr_rawsort = function | RProp Term.Null -> str "Prop" | RProp Term.Pos -> str "Set" - | RType u -> str "Type" ++ pr_opt pr_universe u + | RType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u) let pr_id = pr_id let pr_name = pr_name diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index fa839587f..749534984 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -279,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 @@ -329,7 +333,7 @@ let print_typed_body (val_0,typ) = 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 = Typeops.type_of_constant_type (Global.env()) cb.const_type in hov 0 ( match val_0 with | None -> |