diff options
| author | Emilio Jesus Gallego Arias | 2018-04-27 14:36:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-04-27 14:36:30 +0200 |
| commit | 53fb4203b80da48e2ac9b06803c57e81df702a0a (patch) | |
| tree | 0dc2a8efe8012190fcfcda50faf65365e30a3bad /dev | |
| parent | c65a1637b5e6cb60222963f29fc7c01bd7d1ee0b (diff) | |
| parent | 285bd0778bfa829e1969598cccd5d7c504d5fa90 (diff) | |
Merge PR #7351: Always print explanation for univ inconsistency, rm Flags.univ_print
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f9b4025866..8d5b5bef4a 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -162,8 +162,8 @@ let pp_state_t n = pp (Reductionops.pr_state n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) let ppmetas metas = pp(Termops.pr_metaset metas) -let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd) -let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print None evd) +let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) evd) +let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd) let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars) let ppexistentialset evars = |