diff options
| author | Hugo Herbelin | 2018-10-19 23:34:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-19 23:34:24 +0200 |
| commit | 02f7b4ac1968ca4522d144e34b52dead3871a8b7 (patch) | |
| tree | 1e649e34972959b77eeebd4c5c6237fd12af1f61 /printing/printer.ml | |
| parent | 3799939088b5aa616974a0d37de7e2616024f222 (diff) | |
| parent | 4ac1e342fe420e0b3f3adc9e619d2e98eba2111d (diff) | |
Merge PR #8758: [api] Qualify access to `Nametab`
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 990bdaad7d..3cf995a005 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -15,7 +15,6 @@ open Names open Constr open Environ open Globnames -open Nametab open Evd open Refiner open Constrextern @@ -242,7 +241,7 @@ let pr_abstract_cumulativity_info sigma cumi = (**********************************************************************) (* Global references *) -let pr_global_env = pr_global_env +let pr_global_env = Nametab.pr_global_env let pr_global = pr_global_env Id.Set.empty let pr_universe_instance evd inst = |