diff options
| author | herbelin | 2011-11-16 08:46:49 +0000 |
|---|---|---|
| committer | herbelin | 2011-11-16 08:46:49 +0000 |
| commit | b881c53180533ce0757df2b1572f2fa8df042ee8 (patch) | |
| tree | 9af3579085101b67a808994e7cb1037cd9c92a77 /plugins/syntax/string_syntax.ml | |
| parent | 93b759f35a9f6544c5da9643330beb54ce255619 (diff) | |
Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).
(technically, since the signature "tomatch" of terms to match and of
terms to generalize is typed in a context that does not consider terms
to match as binders while the return predicate do consider them as
binders, the adjusment of the context of the "tomatch" to the context
of the predicate needs lifting in each missing part of the "tomatch"
context, what was not done)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14664 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions