diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-05 14:54:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-05 14:54:26 +0000 |
| commit | 93db5abc5de50a6c43e2b94915cedce29b4a9c02 (patch) | |
| tree | 4ccdcb70f838e91ff8f097d0ae612978a834089a /parsing/pptactic.ml | |
| parent | 2dd11f7fb059a23f15d1a9dec1354edd55a15726 (diff) | |
Correction bug de filtrage sous-terme #1920 introduit dans commit
11126 et qui faisait qu'on ne backtrackait en fait plus sur les
sous-termes d'un terme qui lui filtrait.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11304 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pptactic.ml')
0 files changed, 0 insertions, 0 deletions