aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/dAst.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-27 10:19:40 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-27 10:19:40 +0100
commit37b198dc2ddf2f22e548a60a163607cfc6fbf4b5 (patch)
treecdad1cb00a55d5ce4e0e36d851bad1c3326e04a8 /lib/dAst.mli
parentf6857ce53ecf64b0086854495b4a8451f476d5b4 (diff)
parentb455e96cce263ea48ff0aa8b8ebf530d0f1eea9c (diff)
Merge PR #6040: Making coq_makefile usage consistent with what it claims + possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments)
Diffstat (limited to 'lib/dAst.mli')
0 files changed, 0 insertions, 0 deletions