aboutsummaryrefslogtreecommitdiff
path: root/interp/notation.ml
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-06-17 14:21:51 +0200
committerMatthieu Sozeau2014-06-17 15:42:14 +0200
commit2b7bede68c213fbb884c773c073ba31a886f41f4 (patch)
treebb91ed3f2d7bf0dea38551cd5f7674842398b92d /interp/notation.ml
parentd104b50b9c9a589d9fd8e44bdf56794c8aea4e53 (diff)
Fix a de Bruijn bug in checking code of projections.
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions