diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 2 | ||||
| -rw-r--r-- | dev/include | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 9 |
3 files changed, 7 insertions, 6 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index feef80ed35..fcee79e07e 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -248,6 +248,8 @@ define_evar_* mostly used internally in the unification engine. open Proofview.Notations Proofview.Goal.enter { enter = begin fun gl -> ... end } + +- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` --> `Tacinterp.Value.of_constr c` ========================================= = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = diff --git a/dev/include b/dev/include index b2eb280d6c..d82fb74f22 100644 --- a/dev/include +++ b/dev/include @@ -25,7 +25,7 @@ #cd ".";; #use "base_include";; -#install_printer (* pp_stdcmds *) pppp;; +#install_printer (* pp_stdcmds *) pp;; #install_printer (* pattern *) pppattern;; #install_printer (* glob_constr *) ppglob_constr;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 023835af76..e09477014b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -29,8 +29,7 @@ let _ = set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) (* std_ppcmds *) -let pp x = Feedback.msg_notice x -let pppp x = Feedback.msg_notice x +let pp x = Pp.pp_with !Pp_control.std_ft x (** Future printer *) @@ -316,7 +315,7 @@ let constr_display csr = | Anonymous -> "Anonymous" in - Feedback.msg_notice (str (term_display csr) ++fnl ()) + pp (str (term_display csr) ++fnl ()) open Format;; @@ -514,7 +513,7 @@ let _ = (fun () -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Feedback.msg_notice (CErrors.print e) + e -> pp (CErrors.print e) let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; @@ -530,7 +529,7 @@ let _ = (fun () -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Feedback.msg_notice (CErrors.print e) + e -> pp (CErrors.print e) let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; |