diff options
| -rw-r--r-- | parsing/prettyp.ml | 21 | ||||
| -rw-r--r-- | parsing/prettyp.mli | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 3 |
3 files changed, 14 insertions, 12 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index a95fb67f9..7f8c6a776 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -307,17 +307,16 @@ let pr_mutual_inductive finite indl = hov 0 ( str (if finite then "Inductive " else "CoInductive ") ++ prlist_with_sep (fun () -> fnl () ++ str" with ") - print_one_inductive indl) ++ - fnl () + print_one_inductive indl) -let print_mutual sp = +let print_inductive sp = let (mib,mip) = Global.lookup_inductive (sp,0) in let mipv = mib.mind_packets in let names = list_tabulate (fun x -> (sp,x)) (Array.length mipv) in - pr_mutual_inductive mib.mind_finite names (* ++ + pr_mutual_inductive mib.mind_finite names ++ fnl () ++ fnl () ++ print_inductive_implicit_args sp mipv ++ print_inductive_argument_scopes sp mipv -*) + let print_section_variable sp = let d = get_variable sp in print_named_decl d ++ @@ -328,7 +327,7 @@ let print_body = function | None -> (str"<no body>") let print_typed_body (val_0,typ) = - (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ ++ fnl ()) + (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) @@ -352,8 +351,6 @@ let print_constant with_values sep sp = let print_constant_with_infos sp = print_constant true " = " sp ++ print_name_infos (ConstRef sp) -let print_inductive sp = (print_mutual sp) - let print_syntactic_def sep kn = let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn in let c = Syntax_def.search_syntactic_definition dummy_loc kn in @@ -445,7 +442,11 @@ let print_full_pure_context () = str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ print_body val_0) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> - print_inductive kn ++ str "." ++ fnl () ++ fnl () + let (mib,mip) = Global.lookup_inductive (kn,0) in + let mipv = mib.mind_packets in + let names = list_tabulate (fun x -> (kn,x)) (Array.length mipv) in + pr_mutual_inductive mib.mind_finite names ++ str "." ++ + fnl () ++ fnl () | "MODULE" -> (* TODO: make it reparsable *) let (mp,_,l) = repr_kn kn in @@ -546,7 +547,7 @@ let print_opaque_name qid = else error "not a defined constant" | IndRef (sp,_) -> - print_mutual sp + print_inductive sp | ConstructRef cstr -> let ty = Inductiveops.type_of_constructor env cstr in print_typed_value (mkConstruct cstr, ty) diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 8cd2f9658..84d7a5665 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -40,7 +40,7 @@ val print_eval : (* This function is exported for the graphical user-interface pcoq *) val build_inductive : mutual_inductive -> int -> global_reference * rel_context * types * identifier array * types array -val print_mutual : mutual_inductive -> std_ppcmds +val print_inductive : mutual_inductive -> std_ppcmds val print_name : reference -> std_ppcmds val print_opaque_name : reference -> std_ppcmds val print_about : reference -> std_ppcmds diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 94c6ed1f5..d64fb38e5 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -335,7 +335,8 @@ let init is_ide = end; if !batch_mode then (flush_all(); - if !output_context then Pp.ppnl (Prettyp.print_full_pure_context ()); + if !output_context then + Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ()); Profile.print_profile (); exit 0); Lib.declare_initial_state () |