diff options
Diffstat (limited to 'library/nametab.ml')
| -rw-r--r-- | library/nametab.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 4bb9f104d..0172048af 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -7,6 +7,7 @@ (************************************************************************) open Util +open Compat open Pp open Names open Libnames @@ -18,10 +19,10 @@ exception GlobalizationError of qualid exception GlobalizationConstantError of qualid let error_global_not_found_loc loc q = - Stdpp.raise_with_loc loc (GlobalizationError q) + Loc.raise loc (GlobalizationError q) let error_global_constant_not_found_loc loc q = - Stdpp.raise_with_loc loc (GlobalizationConstantError q) + Loc.raise loc (GlobalizationConstantError q) let error_global_not_found q = raise (GlobalizationError q) |