diff options
| author | herbelin | 2007-10-12 13:36:02 +0000 |
|---|---|---|
| committer | herbelin | 2007-10-12 13:36:02 +0000 |
| commit | f9d7ccaf40f7f21ce0630c9b668581249a635de9 (patch) | |
| tree | 659d29f45c32211ef8bd012353d9100514932c1e /scripts | |
| parent | 5c0beed3886749f7beb1227e8b321828eeae57a1 (diff) | |
Uniformisation du comportement de rewrite et rewrite in : quand le
filtrage d'ordre 2 échoue à trouver un prédicat de réécriture qui
n'est pas une K-abstraction, les deux rewrite essaie alors le filtrage
d'ordre 1. Ce n'est pas le plus élégant mais c'est la solution
uniforme permettant d'être conservatif.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10221 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
0 files changed, 0 insertions, 0 deletions