Hypotheses in [Proofview.Goal.enter] were not normalised.

Fixes PTSF (though I have no idea what caused this bug to show up just yesterday).

1 files changed, 1 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 74f41d0713..08a4d41c97 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -873,6 +873,7 @@ module Goal = struct
     let concl = Reductionops.nf_evar sigma concl in
     let map_nf c = Reductionops.nf_evar sigma c in
     let hyps = Environ.map_named_val map_nf hyps in
+    let env = Environ.reset_with_named_context hyps env in
     f {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self}
   end