aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-08-20 10:25:37 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-08-20 17:45:22 +0200
commit513e194656429b6a9142a3a34095cee2c6f8ee96 (patch)
treea935129d675b538a12102e1cddac453a05f6b76e /tools/coqdoc
parent283579ff70d324296e2b7ee2535b1187ca32e0cb (diff)
Fixing an anomaly in printing a unification error message.
Diffstat (limited to 'tools/coqdoc')
0 files changed, 0 insertions, 0 deletions