diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-05 17:59:10 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-05 17:59:10 +0000 |
| commit | 2e3cf396ba869987c4e41f46bc9b4b2fe31ab4d2 (patch) | |
| tree | 4da162a9a1c2c937f4e12524b13f7f0b76dcb13c /plugins/xml | |
| parent | 87b9f636f602e6067314ac994777e54307a72a65 (diff) | |
Fix a confusion between types of locations in an untyped part of the parser
after the migration of compat.ml4
This was leading to huge positions written to .glob files, making
coqdoc loop forever.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15861 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml')
0 files changed, 0 insertions, 0 deletions