diff options
| author | Maxime Dénès | 2018-07-20 18:01:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-07-26 14:42:45 +0200 |
| commit | f54192a50eaf14852e1462f24e4168aa8a8545fe (patch) | |
| tree | 64696d9c111f420e9bff7d7f742602a6b38f8b0a /printing | |
| parent | 85d5f45d7a5374646a31f8829965bbfed0a95070 (diff) | |
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 7258bb9b72..02968b9d67 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -909,7 +909,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 |