diff options
| author | herbelin | 2011-11-16 08:46:54 +0000 |
|---|---|---|
| committer | herbelin | 2011-11-16 08:46:54 +0000 |
| commit | d305fd7ce51e71ddc49901cb86b7394ea51705d3 (patch) | |
| tree | 45887c3e9c7b1398937149394032a202ef203031 /plugins/syntax/string_syntax.ml | |
| parent | b881c53180533ce0757df2b1572f2fa8df042ee8 (diff) | |
Old generalization bug in pattern-matching: names were considered the
same in every branches while they should have been adjusted to the
names locally used in the branch. Fixing it by remembering an index
of the declaration to abstract in the env together with the
declaration itself.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14666 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions