aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-01-12 10:46:43 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-01-12 14:38:42 +0100
commit682ddc2d278b345c4c72da6c8a8d17cc82a076ec (patch)
treec5dae36d253a66f7714e78a6ebb472b830e06dfb /tools/coqdep.ml
parent4dbf44a47949adce5e538a7aacc670ec64c28d3f (diff)
Documenting option 'Set Bracketing Last Introduction Pattern'.
Diffstat (limited to 'tools/coqdep.ml')
0 files changed, 0 insertions, 0 deletions