diff options
| author | sacerdot | 2004-10-28 11:29:50 +0000 |
|---|---|---|
| committer | sacerdot | 2004-10-28 11:29:50 +0000 |
| commit | 2fa1a1264fcb7aac96692458abbadbacda95d1ad (patch) | |
| tree | 544eea98d9c142c447dcf455a8c158daa39bae32 /kernel | |
| parent | e8f48103b195eab218aa0d83141b1f08e62d9be6 (diff) | |
Added code to get rid of duplicate rewriting rules.
A rule is a duplicate of another rule when their types are alpha convertible.
Eliminating duplicates speed up the tactic (but it slows down the operation
of addition of a new rule that is also performed every time subst_mps is applied
to the module).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6266 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions
