diff options
| -rwxr-xr-x | library/nametab.ml | 2 | ||||
| -rwxr-xr-x | library/nametab.mli | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 4272bda598..aec5da6f90 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -32,6 +32,8 @@ exception GlobalizationError of qualid let error_global_not_found_loc loc q = Stdpp.raise_with_loc loc (GlobalizationError q) +let error_global_not_found q = raise (GlobalizationError q) + (*s Roots of the space of absolute names *) let roots = ref [] diff --git a/library/nametab.mli b/library/nametab.mli index 5e867c11d5..8506c7a5b5 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -36,6 +36,7 @@ exception GlobalizationError of qualid (* Raises a globalization error *) val error_global_not_found_loc : loc -> qualid -> 'a +val error_global_not_found : qualid -> 'a (*s Names tables *) type cci_table = global_reference Idmap.t |