diff options
Diffstat (limited to 'interp/reserve.ml')
| -rw-r--r-- | interp/reserve.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml index 36005121b..b57103cf2 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -22,7 +22,7 @@ open Notation_ops open Globnames type key = - | RefKey of global_reference + | RefKey of GlobRef.t | Oth (** TODO: share code from Notation *) |