diff options
| author | herbelin | 2004-02-12 19:35:23 +0000 |
|---|---|---|
| committer | herbelin | 2004-02-12 19:35:23 +0000 |
| commit | b847fcc99e35a09b862aa758c5e3f0b08a93202d (patch) | |
| tree | a1e88a9123be5255852cc93015fd5b22699633d6 /lib/util.ml | |
| 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/util.ml')
| -rw-r--r-- | lib/util.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index d80f09062c..56d6717e38 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 |