diff options
author | 2008-07-31 19:17:47 +0000 | |
---|---|---|
committer | 2008-07-31 19:17:47 +0000 | |
commit | 0721090dea4d9018f4c4cad8cefa1a10fb0d5a71 (patch) | |
tree | e5d33456ca9e2e98b7cfcc952b834235250f3aa1 /parsing/pptactic.ml | |
parent | 736294486e4d5a4238c98af1ba35e20e59215ee2 (diff) |
Corrige un bug du commit 11187 (le comportement à respecter était
celui-là: si une structure canonique existe déjà avec une certaine
projection canonique donnée, on garde l'ancienne structure si jamais
une structure canonique plus récente arrive avec la même projection
canonique).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11298 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pptactic.ml')
0 files changed, 0 insertions, 0 deletions