diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
commit | f219abfed720305c13875c3c63f9240cf63f78bc (patch) | |
tree | 69d2c026916128fdb50b8d1c0dbf1be451340d30 /lib/stateid.mli | |
parent | 476d60ef0fe0ac015c1e902204cdd7029e10ef0f (diff) | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Merge tag 'upstream/8.5_beta1+dfsg'
Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'lib/stateid.mli')
-rw-r--r-- | lib/stateid.mli | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/lib/stateid.mli b/lib/stateid.mli new file mode 100644 index 00000000..2c12c30c --- /dev/null +++ b/lib/stateid.mli @@ -0,0 +1,45 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Xml_datatype + +type t + +val equal : t -> t -> bool +val compare : t -> t -> int + +module Set : Set.S with type elt = t + +val initial : t +val dummy : t +val fresh : unit -> t +val to_string : t -> string +val of_int : int -> t +val to_int : t -> int +val newer_than : t -> t -> bool + +(* XML marshalling *) +val to_xml : t -> xml +val of_xml : xml -> t + +(* Attaches to an exception the concerned state id, plus an optional + * state id that is a valid state id before the error. + * Backtracking to the valid id is safe. + * The initial_state_id is assumed to be safe. *) +val add : Exninfo.info -> ?valid:t -> t -> Exninfo.info +val get : Exninfo.info -> (t * t) option + +type ('a,'b) request = { + exn_info : t * t; + stop : t; + document : 'b; + loc : Loc.t; + uuid : 'a; + name : string +} + |