diff options
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index abcabe815..9055dcc86 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -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 *) |