diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-10-04 12:35:08 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-10-04 12:35:08 +0200 |
| commit | a44893028eb1dd434c68001234ad56d030205a8e (patch) | |
| tree | 8450dc2022a06bf1911b632e8f5933e7029de179 /backend/Selection.v | |
| parent | 61bd4cf7b75a51912cb885dd3b1d2ef2f7dae1e9 (diff) | |
| download | compcert-kvx-a44893028eb1dd434c68001234ad56d030205a8e.tar.gz compcert-kvx-a44893028eb1dd434c68001234ad56d030205a8e.zip | |
Remove usage of do.
Apparently coq compiled with camlp4 has a problem with the user
defined do <- ... ; ... and do.
Bug 20050
Diffstat (limited to 'backend/Selection.v')
0 files changed, 0 insertions, 0 deletions