aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-12-03 14:48:09 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-12-03 19:26:16 +0100
commit34bb77c953e917f5fbff489c5758abcbadc22224 (patch)
treed92ff3dbde50be1227891b7dde96a1ee3951c6ca /tools/coqdep.ml
parentdfeaea43d9e692984cf430f4f19ec527625586ea (diff)
Slight improving of a unification error message.
Diffstat (limited to 'tools/coqdep.ml')
0 files changed, 0 insertions, 0 deletions