aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.ml
diff options
context:
space:
mode:
authorsacerdot2004-10-28 11:29:50 +0000
committersacerdot2004-10-28 11:29:50 +0000
commit2fa1a1264fcb7aac96692458abbadbacda95d1ad (patch)
tree544eea98d9c142c447dcf455a8c158daa39bae32 /kernel/typeops.ml
parente8f48103b195eab218aa0d83141b1f08e62d9be6 (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/typeops.ml')
0 files changed, 0 insertions, 0 deletions