diff options
| author | Guillaume Melquiond | 2017-04-02 10:30:59 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2017-04-02 10:33:44 +0200 |
| commit | 58bc387700d1fe4856571e8fae5c1761f89adc38 (patch) | |
| tree | e0cf041a35ccbf5315d900e3bf05024bb38c8c96 /kernel/nativecode.ml | |
| parent | 05421cef04206a18cb30f6d115d27e7cb25ba0bf (diff) | |
Simplify some proofs.
This commit does not modify the signature of the involved modules, only
the opaque proof terms.
One has to wonder how proofs can bitrot so much that several occurrences
of "replace 4 with 4" start appearing.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions