diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-12 19:35:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-12 19:35:23 +0000 |
| commit | b847fcc99e35a09b862aa758c5e3f0b08a93202d (patch) | |
| tree | a1e88a9123be5255852cc93015fd5b22699633d6 /lib | |
| parent | dabb8781bf86fb7f85aa4c96928252c6afc8f3cc (diff) | |
Localisation des erreurs d'internalisation des notations de tactiques
dans le module de leur définition.
Error_in_file dans Util et étendu avec possibilité de noms de modules
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 5 | ||||
| -rw-r--r-- | lib/util.mli | 6 |
2 files changed, 11 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index d80f09062..56d6717e3 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -31,6 +31,11 @@ let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm)) let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s) let join_loc (deb1,_) (_,fin2) = (deb1,fin2) +(* Like Exc_located, but specifies the outermost file read, the filename + associated to the location of the error, and the error itself. *) + +exception Error_in_file of string * (bool * string * Util.loc) * exn + (* Projections from triplets *) let pi1 (a,_,_) = a diff --git a/lib/util.mli b/lib/util.mli index 58d5150b7..e4a2ef707 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -41,6 +41,12 @@ val user_err_loc : loc * string * std_ppcmds -> 'a val invalid_arg_loc : loc * string -> 'a val join_loc : loc -> loc -> loc +(* Like [Exc_located], but specifies the outermost file read, the + input buffer associated to the location of the error (or the module name + if boolean is true), and the error itself. *) + +exception Error_in_file of string * (bool * string * loc) * exn + (*s Projections from triplets *) val pi1 : 'a * 'b * 'c -> 'a |