diff options
author | 2017-05-16 02:46:17 +0200 | |
---|---|---|
committer | 2017-05-22 15:22:06 +0200 | |
commit | f1e08dd28903513b71909326d60dc77366dca0fa (patch) | |
tree | e98d52d1c513dff44c14ef5d10cbb6c1c64d71fb /library | |
parent | fdfdbcda1983c229779a09d77ead5033202bfbc7 (diff) |
romega: no more normalization trace, replaced by some Coq-side computation
This is a major change :
- Generated proofs are quite shorter, since only the resolution trace remains.
- No time penalty mesured (it even tends to be slightly faster this way).
- Less infrastructure in ReflOmegaCore and refl_omega.
- Warning: the normalization functions in ML and in Coq should be kept
in sync, as well as the variable order.
- Btw: get rid of ML constructor Oufo
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions