aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.mli
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-11-02 15:40:55 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-11-02 15:40:55 +0000
commit0c7a77321a043a27645b6ec13b39b45aa7de28e7 (patch)
treefb8cb5a6c575d5ebeb21ed6c378486e43fd03430 /proofs/goal.mli
parent056c7c4c33ca20c3185f09fedb9e963cd440907b (diff)
push_rel_context: do not rename section variables.
Renaming section variables is incorrect. And interacts badly with Hints and Canonical Structures in sections. (bug noticed in ssreflect) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17024 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/goal.mli')
0 files changed, 0 insertions, 0 deletions