diff options
| author | Emilio Jesus Gallego Arias | 2019-06-16 17:31:07 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-19 15:17:14 +0200 |
| commit | 8a6a3b4f6cbdaf2047ab30b7eaf451c166a874bc (patch) | |
| tree | ad3ab8b5e988c3d6550843c3b33be610ecc23e68 /kernel/cbytecodes.ml | |
| parent | 041c09d0f59b420285723d000e4ea08fb2d3fb2d (diff) | |
[Fail] Tweaks to implementation.
We handle state restoration outside the main fail logic, as in the
future it could be that vernac execution is fully functional so we
could get rid of the second part.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions