diff options
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 390c3a82e1..a7a8bf5bed 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -29,7 +29,7 @@ open Decl_kinds let dl = Loc.ghost (** Should we keep details of universes during detyping ? *) -let print_universes = ref false +let print_universes = Flags.univ_print (****************************************************************************) (* Tools for printing of Cases *) |