diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index b0fccc42f2..ce7f5959ad 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -101,7 +101,7 @@ let equal evars1 gl1 evars2 gl2 = [evi]. Note: since we want to use it on goals, the body is actually supposed to be empty. *) let contained_in_info sigma e evi = - Evar.Set.mem e (Evarutil.(evars_of_evar_info (nf_evar_info sigma evi))) + Evar.Set.mem e (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) (* [depends_on sigma src tgt] checks whether the goal [src] appears as an existential variable in the definition of the goal [tgt] in [sigma]. *) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 931d4a2b34..2e65aa8d70 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -816,7 +816,7 @@ module V82 = struct let top_evars initial = let evars_of_initial (c,_) = - Evar.Set.elements (Evarutil.evars_of_term c) + Evar.Set.elements (Evd.evars_of_term c) in List.flatten (List.map evars_of_initial initial) |