diff options
| author | Pierre-Marie Pédrot | 2013-11-19 19:50:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-11-22 00:31:15 +0100 |
| commit | 400327165edcba667ebb70ebb89052455656b719 (patch) | |
| tree | bb75fbc10f2c43861e13de90df02e188e64078d3 /dev/base_include | |
| parent | 433fe369bc95d7fe2086cf2256d85443b2420f34 (diff) | |
Using hashes instead of strings in dynamic tags. In case of collision, an
anomaly is raised. As there are very few tags defined in Coq code, this is
very unlikely to appear, and can be fixed by tweaking the name of the
dynamic argument.
This should be more efficient, as we did compare equal strings each time.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions