diff options
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 6cd00c318..42dcbd192 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -56,10 +56,9 @@ let descendent gl e = (* [advance sigma g] returns [Some g'] if [g'] is undefined and is the current avatar of [g] (for instance [g] was changed by [clear] into [g']). It returns [None] if [g] has been (partially) solved. *) -open Store.Field let rec advance sigma g = let evi = Evd.find sigma g.content in - if Option.default false (Evarutil.cleared.get evi.Evd.evar_extra) then + if Option.default false (Evd.Store.get evi.Evd.evar_extra Evarutil.cleared) then let v = match evi.Evd.evar_body with | Evd.Evar_defined c -> c |