diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 39d6a59db..d9a22b3e7 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -378,8 +378,6 @@ type clear_dependency_error = exception ClearDependencyError of Id.t * clear_dependency_error -open Store.Field - let cleared = Store.field () let rec check_and_clear_in_constr evdref err ids c = @@ -448,7 +446,7 @@ let rec check_and_clear_in_constr evdref err ids c = (* 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' = cleared.set true 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 *) |