diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-19 17:08:49 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-19 17:08:49 +0000 |
| commit | 17d347ce043aada5a4a4949434b95fcbed17fe17 (patch) | |
| tree | 6c6defdbd6d275e86251e6dd350f845e89b095b5 /plugins/extraction/miniml.mli | |
| parent | 9d66e886d4c8dcf8b6cb44923d06913161e2cf5c (diff) | |
Extraction: global reference should be indexed on their user part (fix #2540)
Since in Extract_env we recreate constant and mind whose canonical part
might be inaccurate, we shouldn't use an Hashtbl on global_reference
derived from these constant and mind, otherwise equivalent refs could be
considered distinct.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14141 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/miniml.mli')
0 files changed, 0 insertions, 0 deletions