diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 47 | ||||
| -rw-r--r-- | printing/printer.ml | 13 | ||||
| -rw-r--r-- | printing/printer.mli | 2 | ||||
| -rw-r--r-- | printing/printmod.ml | 1 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 1 |
5 files changed, 24 insertions, 40 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index b55a41471a..f9f46e1ceb 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -143,7 +143,8 @@ let tag_var = tag Tag.variable let pr_generalization bk ak c = let hd, tl = match bk with - | Implicit -> "{", "}" + | NonMaxImplicit -> "[", "]" + | MaxImplicit -> "{", "}" | Explicit -> "(", ")" in (* TODO: syntax Abstraction Kind *) str "`" ++ str hd ++ c ++ str tl @@ -223,7 +224,7 @@ let tag_var = tag Tag.variable let pr_opt_type_spc pr = function | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt () - | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t + | t -> str " :" ++ pr_sep_com (fun()->brk(1,4)) (pr ltop) t let pr_prim_token = function | Numeral (SPlus,n) -> str (NumTok.to_string n) @@ -324,12 +325,14 @@ let tag_var = tag Tag.variable let surround_impl k p = match k with | Explicit -> str"(" ++ p ++ str")" - | Implicit -> str"{" ++ p ++ str"}" + | NonMaxImplicit -> str"[" ++ p ++ str"]" + | MaxImplicit -> str"{" ++ p ++ str"}" let surround_implicit k p = match k with | Explicit -> p - | Implicit -> (str"{" ++ p ++ str"}") + | NonMaxImplicit -> str"[" ++ p ++ str"]" + | MaxImplicit -> (str"{" ++ p ++ str"}") let pr_binder many pr (nal,k,t) = match k with @@ -384,12 +387,12 @@ let tag_var = tag Tag.variable if is_open then pr_delimited_binders pr_com_at sep pr_c else pr_undelimited_binders sep pr_c - let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = + let pr_recursive_decl pr pr_dangling kw dangling_with_for id bl annot t c = let pr_body = if dangling_with_for then pr_dangling else pr in - pr_id id ++ (if bl = [] then mt () else str" ") ++ + hov 0 (str kw ++ brk(1,2) ++ pr_id id ++ (if bl = [] then mt () else brk(1,2)) ++ hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++ - pr_opt_type_spc pr t ++ str " :=" ++ + pr_opt_type_spc pr t ++ str " :=") ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c let pr_guard_annot pr_aux bl ro = @@ -404,28 +407,28 @@ let tag_var = tag Tag.variable | CLocalPattern _ -> assert false in let ids = List.flatten (List.map names_of_binder bl) in if List.length ids > 1 then - spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" + spc() ++ str "{" ++ keyword "struct" ++ brk (1,1) ++ pr_id id ++ str"}" else mt() | CWfRec (id,c) -> - spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_lident id ++ str"}" + spc() ++ str "{" ++ keyword "wf" ++ brk (1,1) ++ pr_aux c ++ brk (1,1) ++ pr_lident id ++ str"}" | CMeasureRec (id,m,r) -> - spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ - match id with None -> mt() | Some id -> spc () ++ pr_lident id ++ + spc() ++ str "{" ++ keyword "measure" ++ brk (1,1) ++ pr_aux m ++ + match id with None -> mt() | Some id -> brk (1,1) ++ pr_lident id ++ (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" - let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) = + let pr_fixdecl pr prd kw dangling_with_for ({v=id},ro,bl,t,c) = let annot = pr_guard_annot (pr lsimpleconstr) bl ro in - pr_recursive_decl pr prd dangling_with_for id bl annot t c + pr_recursive_decl pr prd kw dangling_with_for id bl annot t c - let pr_cofixdecl pr prd dangling_with_for ({v=id},bl,t,c) = - pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c + let pr_cofixdecl pr prd kw dangling_with_for ({v=id},bl,t,c) = + pr_recursive_decl pr prd kw dangling_with_for id bl (mt()) t c - let pr_recursive pr_decl id = function + let pr_recursive kw pr_decl id = function | [] -> anomaly (Pp.str "(co)fixpoint with no definition.") - | [d1] -> pr_decl false d1 + | [d1] -> pr_decl kw false d1 | dl -> - prlist_with_sep (fun () -> fnl() ++ keyword "with" ++ spc ()) - (pr_decl true) dl ++ + prlist_with_sep (fun () -> fnl()) + (pr_decl "with" true) dl ++ fnl() ++ keyword "for" ++ spc () ++ pr_id id let pr_asin pr na indnalopt = @@ -491,15 +494,13 @@ let tag_var = tag Tag.variable return (pr_cref r us, latom) | CFix (id,fix) -> return ( - hov 0 (keyword "fix" ++ spc () ++ - pr_recursive + hv 0 (pr_recursive "fix" (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v fix), lfix ) | CCoFix (id,cofix) -> return ( - hov 0 (keyword "cofix" ++ spc () ++ - pr_recursive + hv 0 (pr_recursive "cofix" (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v cofix), lfix ) diff --git a/printing/printer.ml b/printing/printer.ml index 97e0528939..cc83a1dde0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -38,7 +38,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "printing of unfocused goal"; optkey = ["Printing";"Unfocused"]; optread = (fun () -> !enable_unfocused_goal_printing); optwrite = (fun b -> enable_unfocused_goal_printing:=b) } @@ -49,7 +48,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "printing of goal tags"; optkey = ["Printing";"Goal";"Tags"]; optread = (fun () -> !enable_goal_tags_printing); optwrite = (fun b -> enable_goal_tags_printing:=b) } @@ -59,7 +57,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "printing of goal names"; optkey = ["Printing";"Goal";"Names"]; optread = (fun () -> !enable_goal_names_printing); optwrite = (fun b -> enable_goal_names_printing:=b) } @@ -416,7 +413,6 @@ let () = let open Goptions in declare_int_option { optdepr = false; - optname = "the hypotheses limit"; optkey = ["Hyps";"Limit"]; optread = (fun () -> !print_hyps_limit); optwrite = (fun x -> print_hyps_limit := x) } @@ -625,7 +621,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "Printing Dependent Evars Line"; optkey = ["Printing";"Dependent";"Evars";"Line"]; optread = (fun () -> !should_print_dependent_evars); optwrite = (fun v -> should_print_dependent_evars := v) } @@ -859,8 +854,6 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) - | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism - on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = @@ -880,13 +873,10 @@ struct Constant.CanOrd.compare k1 k2 | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 - | TemplatePolymorphic m1, TemplatePolymorphic m2 -> - MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 -> GlobRef.Ordered.compare k1 k2 | _ , Constant _ -> 1 | _ , Positive _ -> 1 - | _, TemplatePolymorphic _ -> 1 | _ -> -1 let compare x y = @@ -947,9 +937,6 @@ let pr_assumptionset env sigma s = hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") | Guarded gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.") - | TemplatePolymorphic m -> - hov 2 (safe_pr_inductive env m ++ spc () ++ - strbrk"is assumed template polymorphic on all its universe parameters.") | TypeInType gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") in diff --git a/printing/printer.mli b/printing/printer.mli index 1d7a25cbb6..cd5151bd8f 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -231,8 +231,6 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) - | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism - on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = diff --git a/printing/printmod.ml b/printing/printmod.ml index 85bb287c22..a5fd7f69ed 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -44,7 +44,6 @@ let short = ref false let () = declare_bool_option { optdepr = false; - optname = "short module printing"; optkey = ["Short";"Module";"Printing"]; optread = (fun () -> !short) ; optwrite = ((:=) short) } diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index dec87f8071..d93dd15f91 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -69,7 +69,6 @@ let write_diffs_option opt = let () = Goptions.(declare_string_option { optdepr = false; - optname = "show diffs in proofs"; optkey = ["Diffs"]; optread = read_diffs_option; optwrite = write_diffs_option |