diff options
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index abcabe8157..96e4b6acce 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 @@ -244,6 +244,9 @@ val restrict : evar -> Filter.t -> ?candidates:constr list -> (** Restrict an undefined evar into a new evar by filtering context and possibly limiting the instances to a set of candidates *) +val is_restricted_evar : evar_info -> evar option +(** Tell if an evar comes from restriction of another evar, and if yes, which *) + val downcast : evar -> types -> evar_map -> evar_map (** Change the type of an undefined evar to a new type assumed to be a subtype of its current type; subtyping must be ensured by caller *) |