diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/declare.ml b/library/declare.ml index 6999ee669..d5dc01cf5 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -431,7 +431,7 @@ let strength_of_global = function | IndRef _ | ConstructRef _ | ConstRef _ -> Global let library_part ref = - let sp = Nametab.sp_of_global None ref in + let sp = Nametab.sp_of_global ref in let dir,_ = repr_path sp in match strength_of_global ref with | Local -> |