diff options
| author | Gaëtan Gilbert | 2017-09-29 15:46:14 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-09-29 20:30:43 +0200 |
| commit | 95cd90c7e552b4362201abf671c68c5fbe950547 (patch) | |
| tree | 5e77e3686097630272ef96c6daeb7235b00b1a6d /engine | |
| parent | 423ee45f91a88582983d0cc1928708dba5391ca7 (diff) | |
Remove TODO comment (Evar.t is opaque)
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index abcabe8157..8c8e09eee1 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 |