diff options
| author | herbelin | 2013-06-02 21:31:30 +0000 |
|---|---|---|
| committer | herbelin | 2013-06-02 21:31:30 +0000 |
| commit | 792a07d519a8dd396674e5431af2380a26d74b9c (patch) | |
| tree | 6454d15eee9f3c492a6ce7111692a78cfa38b95c /plugins/syntax/string_syntax.ml | |
| parent | 164b3bdb69f60b9bbbe83abce73c6256869d1f4b (diff) | |
Fixing buggy backtracking in "intros * pat" with failing "pat".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16549 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions