diff options
Diffstat (limited to 'checker/print.ml')
| -rw-r--r-- | checker/print.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/print.ml b/checker/print.ml index da8a6106f..c0d1ac368 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -10,7 +10,7 @@ open Format open Cic open Names -let print_instance i = Pp.pp (Univ.Instance.pr i) +let print_instance i = Feedback.msg_notice (Univ.Instance.pr i) let print_pure_constr csr = let rec term_display c = match c with @@ -108,7 +108,7 @@ let print_pure_constr csr = and sort_display = function | Prop(Pos) -> print_string "Set" | Prop(Null) -> print_string "Prop" - | Type u -> print_string "Type("; Pp.pp (Univ.pr_uni u); print_string ")" + | Type u -> print_string "Type("; Feedback.msg_notice (Univ.pr_uni u); print_string ")" and name_display = function | Name id -> print_string (Id.to_string id) |