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 /pretyping | |
| parent | c65a1637b5e6cb60222963f29fc7c01bd7d1ee0b (diff) | |
| parent | 285bd0778bfa829e1969598cccd5d7c504d5fa90 (diff) | |
Merge PR #7351: Always print explanation for univ inconsistency, rm Flags.univ_print
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index bb563220b6..56e5828918 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -36,7 +36,7 @@ type _ delay = | Later : [ `thunk ] delay (** Should we keep details of universes during detyping ? *) -let print_universes = Flags.univ_print +let print_universes = ref false (** If true, prints local context of evars, whatever print_arguments *) let print_evar_arguments = ref false |