diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-17 18:20:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-18 18:56:39 +0200 |
| commit | e8a531dfa623e3badc3baddcf13f0a7975c37886 (patch) | |
| tree | bfd59d295e477975d8bd49024011ec8d265154ce /proofs | |
| parent | 602544c70684794e34030757ff986eaa5b519069 (diff) | |
Factorizing cutrewrite (to be made obsolote) and dependent rewrite (to
integrate to "rewrite"?) with the code of "replace".
Incidentally, "inversion" relies on dependent rewrite, with an
incompatibility introduced. Left-to-right rewriting is now done with
"eq_rec_r" while before it was done using "eq_rec" of "eq_sym". The
first one reduces to the second one but simpl is not anymore able to
reduce "eq_rec_r eq_refl". Hopefully cbn is able to do it (see
Zdigits).
Diffstat (limited to 'proofs')
0 files changed, 0 insertions, 0 deletions