aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pptactic.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-04-10 16:36:36 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-04-10 16:36:36 +0000
commit8aa6ed2d10ddefb348f98684e691e25e4866b6ca (patch)
treec286ad9f175e2c3088ea162da9df649134e15fa4 /parsing/pptactic.ml
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 'parsing/pptactic.ml')
0 files changed, 0 insertions, 0 deletions