diff options
author | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:40:32 +0000 |
---|---|---|
committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:40:32 +0000 |
commit | a92a276d9aadf321262e5b767a809642708c5cc5 (patch) | |
tree | bcfdf7e0e94481ff9a171056baf749c277b18dbb /theories/ZArith | |
parent | 8ead702b4f0ec5e0fecfc5de68f7ce86f56b20fe (diff) |
Fix the compilation of pattern matching wrt to variables.
Compilation of pattern-matching used to systematically introduce a dummy alias x:=x in the typing environment for each variable x in the patterns (except for purely variable patterns which correctly alias the term being matched). This interfered badly with the new refine implementation.
To correct this I changed the "all variables" case of pattern-matching compilation to check whether the term currently being matched is a term introduced by the user or a subterm which is necessarily a variable. In the latter case, no alias is introduced.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17020 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
0 files changed, 0 insertions, 0 deletions