aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/metasyntax.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-26 14:56:28 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-26 14:56:28 +0200
commit51d418636adf30bcf4e37a5b7b479a7d54dbedb2 (patch)
tree0ccc548e3322db7b07fbab40aa834b9ca1bf9446 /vernac/metasyntax.ml
parent4d54945d8df4b9b3c0bca17f5bd4d391d7012c8f (diff)
parent8dc130ed11373928f18adc16e552d650209de75f (diff)
Merge PR #868: Fix debug trace of typeclasses eauto.
Diffstat (limited to 'vernac/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions