aboutsummaryrefslogtreecommitdiffhomepage
path: root/build
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-11-09 19:59:13 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-11-09 20:04:25 +0100
commit07f0871dde38d6e5bfa57a36071e72ca7c207a39 (patch)
tree72d54fc38434235a45c9ed1beb89d0408ed9ee06 /build
parentce80fa3cb3e6d8809bb3ee015bff39c67c0aed16 (diff)
Fixing bug #3792.
Pretyping of [if] cases was missing a convertibility check with the ambient type constraint, and just dropped it. This was making the pretyper construct ill-typed terms.
Diffstat (limited to 'build')
0 files changed, 0 insertions, 0 deletions