aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-08-05 14:54:26 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-08-05 14:54:26 +0000
commit93db5abc5de50a6c43e2b94915cedce29b4a9c02 (patch)
tree4ccdcb70f838e91ff8f097d0ae612978a834089a /toplevel
parent2dd11f7fb059a23f15d1a9dec1354edd55a15726 (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 'toplevel')
0 files changed, 0 insertions, 0 deletions