diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/compat.ml4 | 1 | ||||
| -rw-r--r-- | lib/util.ml | 21 | ||||
| -rw-r--r-- | lib/util.mli | 19 |
3 files changed, 24 insertions, 17 deletions
diff --git a/lib/compat.ml4 b/lib/compat.ml4 new file mode 100644 index 0000000000..57c7915e30 --- /dev/null +++ b/lib/compat.ml4 @@ -0,0 +1 @@ +type loc = int * int let dummy_loc = 0, 0 let unloc x = x let make_loc x = x diff --git a/lib/util.ml b/lib/util.ml index 9c51f3968f..1aa3786f2c 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1,10 +1,10 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) @@ -22,10 +22,13 @@ let errorlabstrm l pps = raise (UserError(l,pps)) let todo s = prerr_string ("TODO: "^s^"\n") +type loc = Compat.loc +let dummy_loc = Compat.dummy_loc +let unloc = Compat.unloc +let make_loc = Compat.make_loc + (* raising located exceptions *) -type loc = int * int type 'a located = loc * 'a -let dummy_loc = (0,0) let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm)) 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) diff --git a/lib/util.mli b/lib/util.mli index 79133a930c..45e953a649 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -1,10 +1,10 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) @@ -32,9 +32,12 @@ val errorlabstrm : string -> std_ppcmds -> 'a val todo : string -> unit -type loc = int * int +type loc = Compat.loc + type 'a located = loc * 'a +val unloc : loc -> int * int +val make_loc : int * int -> loc val dummy_loc : loc val anomaly_loc : loc * string * std_ppcmds -> 'a val user_err_loc : loc * string * std_ppcmds -> 'a |