aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-09 15:33:45 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-09 15:33:45 +0200
commitd5534aab708e5d3bd6c3633dc9d028016eeb3076 (patch)
treeb74bcffce9869dc8aaec115e4614fb7e89ac5a3d /engine
parent73a858469479651cc4baf631a45a9ff1d69d0c66 (diff)
parentd19e8bafe6cc18cc47bbb3e3f7aa0d2d719014c0 (diff)
Merge PR #1109: Handle some misc todos
Diffstat (limited to 'engine')
-rw-r--r--engine/evd.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index 9055dcc86..96e4b6acc 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -31,7 +31,7 @@ open Environ
(** {6 Evars} *)
type evar = existential_key
-(** Existential variables. TODO: Should be made opaque one day. *)
+(** Existential variables. *)
val string_of_existential : evar -> string