diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-31 09:09:56 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-31 09:11:27 +0200 |
| commit | b994e3195d296e9d12c058127ced381976c3a49e (patch) | |
| tree | 8648a92470d27671db9d5e40159a1aec68e8dc9c /checker/print.ml | |
| parent | 7d2ad6ac66abb97819ffbc5ad58c862a84e28775 (diff) | |
Checker: avoid using obsolete names from Names
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 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 |