diff options
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index a9aa4fa59..df3f6e0db 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -464,17 +464,17 @@ module V82 = struct (* Old style env primitive *) let env evars gl = let evi = content evars gl in - Evd.evar_env evi + Evd.evar_filtered_env evi (* For printing *) let unfiltered_env evars gl = let evi = content evars gl in - Evd.evar_unfiltered_env evi + Evd.evar_env evi (* Old style hyps primitive *) let hyps evars gl = let evi = content evars gl in - evi.Evd.evar_hyps + Evd.evar_hyps evi (* Access to ".evar_concl" *) let concl evars gl = |