diff options
| author | letouzey | 2011-09-07 17:04:03 +0000 |
|---|---|---|
| committer | letouzey | 2011-09-07 17:04:03 +0000 |
| commit | 0837909e773b1229408e2f9eac26cbde6ba759de (patch) | |
| tree | 87611efa5dac6b7828914960fbbed627de4ccf1e /plugins/xml/xmlcommand.ml | |
| parent | 8421370e3b467799805b0b1289630228859aca1a (diff) | |
Fix the hconsing of universes
Two issues were preventing the hcons1_univ function to properly work
- a launch of Names.hcons_names () at each hconsing of universe,
hence one separated hash-table for dir-path created at each time,
oups...
- Bad handling of the universe sub-structure universe_level
To check : is there an interest in making separate calls to
Names.hcons_names () in separate places (Univ, Term, Declare) ?
I think not. Btw the hconsing of Declare.hcons_constant_declaration
is also probably wrong. To be fixed in a forthcoming patch.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14463 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions