aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-05-26 13:30:38 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-05-26 13:33:06 +0200
commit525094414bf74445f930e170a823a49107726f6f (patch)
treeb15177a6580ff221dbe9d52442b59b1a271155b8 /tools/coqdep.ml
parent1f0284e591c7315149509200239fc9c821c2c9dd (diff)
Fixing commit 9cef834. The parsing rules were generating an empty list,
conflicting with the previous behaviour of 'eexists'.
Diffstat (limited to 'tools/coqdep.ml')
0 files changed, 0 insertions, 0 deletions