diff options
author | 2015-01-25 14:42:51 +0100 | |
---|---|---|
committer | 2015-01-25 14:42:51 +0100 | |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /kernel/evar.mli | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'kernel/evar.mli')
-rw-r--r-- | kernel/evar.mli | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/kernel/evar.mli b/kernel/evar.mli new file mode 100644 index 00000000..2c94db3f --- /dev/null +++ b/kernel/evar.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This module defines existential variables, which are isomorphic to [int]. + Nonetheless, casting from an [int] to a variable is deemed unsafe, so that + to keep track of such casts, one has to use the provided {!unsafe_of_int} + function. *) + +type t +(** Type of existential variables. *) + +val repr : t -> int +(** Recover the underlying integer. *) + +val unsafe_of_int : int -> t +(** This is not for dummies. Do not use this function if you don't know what you + are doing. *) + +val equal : t -> t -> bool +(** Equality over existential variables. *) + +val compare : t -> t -> int +(** Comparison over existential variables. *) + +val hash : t -> int +(** Hash over existential variables. *) + +module Set : Set.S with type elt = t +module Map : CMap.ExtS with type key = t and module Set := Set |