diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-16 02:46:17 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 15:22:06 +0200 |
| commit | f1e08dd28903513b71909326d60dc77366dca0fa (patch) | |
| tree | e98d52d1c513dff44c14ef5d10cbb6c1c64d71fb /COPYRIGHT | |
| 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 'COPYRIGHT')
0 files changed, 0 insertions, 0 deletions