diff options
| author | Maxime Dénès | 2017-10-05 18:27:24 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-05 18:27:24 +0200 |
| commit | 6c177d95f4e7d3179db1732f1ba1bda43a83393f (patch) | |
| tree | a201827ca42ae9148585c575ede2c0f2dc30dc89 /engine/evd.mli | |
| parent | 8ce4b0d7d16fe134d8621efc9d557ba3e9686b0f (diff) | |
| parent | 05bd0ab1dd85764874ca077005dcaff5414589a5 (diff) | |
Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5757)
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 abcabe8157..9055dcc86b 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 *) |