diff options
| author | aspiwack | 2013-11-02 15:39:57 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:39:57 +0000 |
| commit | 9cdadde0422382852eddefa17201778606256f2f (patch) | |
| tree | f7f16568ff307ab130cad7545760171ec1f0a6f9 /kernel/nativecode.ml | |
| parent | c9504af26647ab745dc22811a2db8058e0b66632 (diff) | |
Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used at the wrong time.
The bug was masked by the fact that Tacinterp uses many superfluous Proofview.Goal.enter, it so happens that the tactic
Proofview.Goal.enter (fun _ -> Proofview.Goal.enter fun gl -> t))
had the correct semantics!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17014 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions