diff options
| author | Hugo Herbelin | 2017-01-26 00:53:23 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-01-26 00:57:02 +0100 |
| commit | 180775636f5ec93e95df681951fafb321f8ebe67 (patch) | |
| tree | adcec1b329ec49b23c3c964890bf19319bc42ffb /stm/asyncTaskQueue.ml | |
| parent | e7bb95f2ac0d151cfdccea7b769413b332489cd3 (diff) | |
Fixing #5326 (anomaly on some unsupported case of 'pat).
We complete the support of 'pat in this particular case (a 'pat under
a binder in a notation).
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions