aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nametab.ml
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-12-06 14:24:53 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-12-06 14:24:53 +0000
commit3e3fa18a066feae44c10fc6e072059f4e9914656 (patch)
tree6ff163fd7561bf8c0823c7508acf83b350d4511d /library/nametab.ml
parentfb75bd254df2eadfc8abd45a646dfe9b1c4a53b6 (diff)
Commit intermédiaire express de réparation de coqide.ml, que j'avais
tout cassé hier sans m'en rendre compte (le soucis de travailler sur un ordinateur où j'ai pas installé lablgtk2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10347 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.ml')
0 files changed, 0 insertions, 0 deletions