diff options
| -rw-r--r-- | proofs/goal.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 2e7ee10bc0..5601cef823 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -355,6 +355,7 @@ let defs _ rdefs _ _ = !rdefs let enter f = (); fun env rdefs gl info -> + let info = Evarutil.nf_evar_info !rdefs info in f env !rdefs (Evd.evar_hyps info) (Evd.evar_concl info) gl (*** Conversion in goals ***) |