aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorherbelin2007-04-10 16:36:36 +0000
committerherbelin2007-04-10 16:36:36 +0000
commit8aa6ed2d10ddefb348f98684e691e25e4866b6ca (patch)
treec286ad9f175e2c3088ea162da9df649134e15fa4 /dev/base_include
parent1fcdaed7fea598ff2724095c5476e8bdc04ef48a (diff)
Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5
tout en évitant que les .. soient dans constr) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9755 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions