aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/uState.mli
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-02 14:58:00 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-06 13:41:24 +0100
commit5d926b0279f70250db1ee54edcdb4e855ac96f0f (patch)
tree06dc436ba2d41764b5bbe48c311bdaeaf5c1514c /engine/uState.mli
parent67a28c487fc64e2c0f8271b77d0c9db0cd82fa92 (diff)
Deprecate UState aliases in Evd.
Diffstat (limited to 'engine/uState.mli')
-rw-r--r--engine/uState.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/uState.mli b/engine/uState.mli
index 68fe350c0..ef7cee32e 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -26,6 +26,8 @@ val empty : t
val make : UGraph.t -> t
+val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t
+
val is_empty : t -> bool
val union : t -> t -> t