diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-26 16:37:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-27 00:28:50 +0200 |
| commit | 05bd0ab1dd85764874ca077005dcaff5414589a5 (patch) | |
| tree | 40ecae5fc60a644761898bcb61e13ef463efecb6 /engine/evd.mli | |
| parent | b818c00e3e895ea9b736ab968e3ba109b0fd67c1 (diff) | |
Moving setting of "cleared" evar flag directly in Evd.restrict.
In particular, this fixes #5757 which used restrict_evar to refine the
information on the source of an evar, and which should have set the
"cleared" flag.
Also renaming flag "restricted" since it is not only about "clear".
I guess this is what we want in general, but I did not survey all uses
of restrict_evar so, maybe, this should be refined further.
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 *) |