diff options
| author | Maxime Dénès | 2017-04-05 18:18:56 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-06 16:07:17 +0200 |
| commit | 48c44b55b76e75aa2af9f82753c6ffe7531790c8 (patch) | |
| tree | 8fe915bd35b77ab231c90e67adf67d6a029155e4 /kernel/nativecode.ml | |
| parent | 33f40197e6b7bef02c8df2dc0a0066f8144b66d6 (diff) | |
Fix a few programming pearls related to Time, Fail and Redirect.
This fixes a few clear bugs, but the STM code handling Time, Fail and
Redirect before par: still needs to be rewritten. It does not implement
the same semantics as the vernac interpreter for Fail Fail [c] and
ignores Redirect.
This commit was already reviewed with Enrico and tested on Travis.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions