aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/print.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/print.ml')
-rw-r--r--checker/print.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/print.ml b/checker/print.ml
index 9cd8fda5d..da8a6106f 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -122,7 +122,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 +131,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