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/evarutil.ml | |
| 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/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 17 |
1 files changed, 3 insertions, 14 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 339c6a248..eabfb7b39 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -478,8 +478,6 @@ type clear_dependency_error = exception ClearDependencyError of Id.t * clear_dependency_error -let cleared = Store.field () - exception Depends of Id.t let rec check_and_clear_in_constr env evdref err ids global c = @@ -552,13 +550,6 @@ let rec check_and_clear_in_constr env evdref err ids global c = let evd = !evdref in let (evd,_) = restrict_evar evd evk filter None in evdref := evd; - (* spiwack: hacking session to mark the old [evk] as having been "cleared" *) - let evi = Evd.find !evdref evk in - let extra = evi.evar_extra in - let extra' = Store.set extra cleared true in - let evi' = { evi with evar_extra = extra' } in - evdref := Evd.add !evdref evk evi' ; - (* spiwack: /hacking session *) Evd.existential_value !evdref ev | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c @@ -665,11 +656,9 @@ let rec advance sigma evk = match evi.evar_body with | Evar_empty -> Some evk | Evar_defined v -> - if Option.default false (Store.get evi.evar_extra cleared) then - let (evk,_) = Term.destEvar v in - advance sigma evk - else - None + match is_restricted_evar evi with + | Some evk -> advance sigma evk + | None -> None (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. |