From 05bd0ab1dd85764874ca077005dcaff5414589a5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 26 Sep 2017 16:37:26 +0200 Subject: 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. --- engine/evd.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'engine/evd.mli') 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 *) -- cgit v1.2.3