diff options
| author | Abhishek Anand (optiplex7010@home) | 2020-02-20 19:52:39 -0800 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-23 18:05:00 +0100 |
| commit | 38c47ac0626fed51d17bc7513d7dbbd63053016e (patch) | |
| tree | 995ead018d1c30343b925ea45a8ffa3bb5124845 | |
| parent | 0dc4b008c753fa4e20ea95630edea9e3e32c68c0 (diff) | |
added the new option
| -rw-r--r-- | interp/constrextern.ml | 4 | ||||
| -rw-r--r-- | interp/constrextern.mli | 1 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
4 files changed, 13 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 38dc10a9b3..a5e7b89ded 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -57,6 +57,10 @@ let print_implicits_defensive = ref true (* This forces printing of coercions *) let print_coercions = ref false +(* This forces printing of parentheses even when + it is implied by associativity/precedence *) +let print_parens = ref false + (* This forces printing universe names of Type{.} *) let print_universes = Detyping.print_universes diff --git a/interp/constrextern.mli b/interp/constrextern.mli index fa263cbeb7..2691d27f69 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -53,6 +53,7 @@ val print_implicits_defensive : bool ref val print_arguments : bool ref val print_evar_arguments : bool ref val print_coercions : bool ref +val print_parens : bool ref val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 65b4e238de..ed54e046fd 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -85,7 +85,7 @@ let tag_var = tag Tag.variable let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in let pop r = let a = List.hd !r in r := List.tl !r; a in let return unp pp1 pp2 = (tag_unparsing unp pp1) ++ pp2 in - let parens = !Constrextern.print_coercions in + let parens = !Constrextern.print_parens in (* Warning: The following function enforces a very precise order of evaluation of sub-components. diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 63fc587f71..cd8e699066 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1282,6 +1282,13 @@ let () = let () = declare_bool_option { optdepr = false; + optkey = ["Printing";"Parens"]; + optread = (fun () -> !Constrextern.print_parens); + optwrite = (fun b -> Constrextern.print_parens := b) } + +let () = + declare_bool_option + { optdepr = false; optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Detyping.print_evar_arguments); optwrite = (:=) Detyping.print_evar_arguments } |