diff options
Diffstat (limited to 'printing/prettyp.ml')
| -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 1f17d844f..b95691031 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -328,7 +328,7 @@ type 'a locatable_info = { type locatable = Locatable : 'a locatable_info -> locatable type logical_name = - | Term of global_reference + | Term of GlobRef.t | Dir of global_dir_reference | Syntactic of KerName.t | ModuleType of ModPath.t |