aboutsummaryrefslogtreecommitdiffhomepage
path: root/install.sh
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-10 22:54:07 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-10 22:54:07 +0000
commitb5d891154620e7f198059401344ee8f5488d077d (patch)
tree09d3d3f25fd08f7f33408481bb0701a35a272b99 /install.sh
parent04a28435e4e3dc9467dca72abb3a8b81268df983 (diff)
Hash-cons the statically allocated Rels (1 to 16) to themselves
This is just a minor detail, but if we take care to use in mkRel always the same physical Rels for n <= 16, then let's ensure that these Rels are preserved by hash-consing. This way, we avoid killing some sharing during hash-consing of most of constr but not all (for instance those in mind). In fact, this is probably superfluous since earlier commit about "| Rel n as t -> t", but let's be sure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14542 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'install.sh')
0 files changed, 0 insertions, 0 deletions