diff options
| author | herbelin | 2011-11-16 08:46:59 +0000 |
|---|---|---|
| committer | herbelin | 2011-11-16 08:46:59 +0000 |
| commit | b05a492a6bd54521c47a72a07bf632ea7a7c8a73 (patch) | |
| tree | 602e62271a14ceae500af91e7d8bc531cc2a5254 /dev/include | |
| parent | 1c9181976f9af6c276bf1c3b9e9e007b981574e3 (diff) | |
Adding postprocessing to remove "commutative cuts" expansions in
pattern-matching when it turns after typing phase that no dependencies exists.
Incidentally, renamed regeneralize_index into relocate_index and make
it works both way (to generalize and to ungeneralize). This avoids
using replace_tomatch for ungeneralization which does not support
modifying the "deps".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14669 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions