diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /checker/print.ml | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'checker/print.ml')
-rw-r--r-- | checker/print.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/checker/print.ml b/checker/print.ml index 9cd8fda5..7ef752b0 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -10,7 +10,9 @@ open Format open Cic open Names -let print_instance i = Pp.pp (Univ.Instance.pr i) +let chk_pp = Pp.pp_with Format.std_formatter + +let print_instance i = chk_pp (Univ.Instance.pr i) let print_pure_constr csr = let rec term_display c = match c with @@ -108,7 +110,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("; chk_pp (Univ.pr_uni u); print_string ")" and name_display = function | Name id -> print_string (Id.to_string id) @@ -122,7 +124,7 @@ let print_pure_constr csr = | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (debug_string_of_mind sp) + print_string (MutInd.debug_to_string sp) and sp_con_display sp = (* let dir,l = decode_kn sp in let ls = @@ -131,7 +133,7 @@ let print_pure_constr csr = | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (debug_string_of_con sp) + print_string (Constant.debug_to_string sp) in try |