diff options
| author | Enrico Tassi | 2018-07-27 08:55:30 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-07-27 08:55:30 +0200 |
| commit | e7c1b08bbb300d31e82ca6c457fd4e3050239b9d (patch) | |
| tree | 6813ef46499b6de0d532d97946374e274e587b58 /printing | |
| parent | 9f9a7736c24270a3f3d8177c65e80a1ee04c4615 (diff) | |
| parent | baf8b6e100c49635c56308f17275b963d4f5253c (diff) | |
Merge PR #8103: Coercions cleanup: use GlobRef.t instead of constr
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 8b835310de..1810cc6588 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -902,7 +902,7 @@ let inspect env sigma depth = open Classops -let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v) +let print_coercion_value env sigma v = Printer.pr_global v.coe_value let print_class i = let cl,_ = class_info_from_index i in |