aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
authorherbelin2006-04-26 22:23:37 +0000
committerherbelin2006-04-26 22:23:37 +0000
commit519804c3de605b6da3c5973cf2061a01d1102270 (patch)
treeb4510f3e1a4f1c1158995ba2c85d6181434dc067 /scripts
parent328be738c63b10638c8826922dd8f28c59b35fe9 (diff)
Diverses corrections de l'afficheur et du traducteur pour s'assurer de
la réversibilité de la traduction (correction enregistrement des retours chariot dans le lexeur, correction affichage espace superflu en tête des VERNAC EXTEND, correction affichage morphism_signature dans extraargs.ml4, correction affichage clear dans pptactic.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8739 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
0 files changed, 0 insertions, 0 deletions