From fb29084052da03308fe45a918c55b86627ba54b6 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 7 Aug 2014 08:10:13 +0200 Subject: Hypotheses in [Proofview.Goal.enter] were not normalised. Fixes PTSF (though I have no idea what caused this bug to show up just yesterday). --- proofs/proofview.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'proofs') diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 74f41d071..08a4d41c9 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 -- cgit v1.2.3