aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Notations2.v
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-07 11:04:46 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-07 11:04:46 +0000
commit92a5f74259977cc3f92d8b822bdb727a95e64bc6 (patch)
treefbe2bd20200ac9de7c89c6a8752f3f007ed06b30 /test-suite/output/Notations2.v
parent5de2bbd213eb770ba465c67103004d9286444a63 (diff)
Extraction: unfolds the let-in created by Program when handling "match"
This leads to code closer to the original input of the user, and moreover some more dummy __ may be removed this way. To avoid unfolding by mistake user's variables, we change the name of these generated let-in into "program_branch_NN" instead of "branch_NN" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13964 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Notations2.v')
0 files changed, 0 insertions, 0 deletions