diff options
| author | bertot | 2003-03-06 07:30:36 +0000 |
|---|---|---|
| committer | bertot | 2003-03-06 07:30:36 +0000 |
| commit | 8b1e3ffdca68c46e2019b49c1c1bcbcd07cb5776 (patch) | |
| tree | 686d7bd172797854fec0e2e0732a5fb8b8d10c05 /ide/undo.ml | |
| parent | 4143f9de648fa618a75804f1202f6daa0a85f718 (diff) | |
Make sure that identifiers are parsed as qualified identifier and that
the whole text is considered, not only the prefix that can be considered as
an identifier.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3745 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/undo.ml')
0 files changed, 0 insertions, 0 deletions