diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-12 10:46:43 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-12 14:38:42 +0100 |
commit | 682ddc2d278b345c4c72da6c8a8d17cc82a076ec (patch) | |
tree | c5dae36d253a66f7714e78a6ebb472b830e06dfb /tools/coqdep.ml | |
parent | 4dbf44a47949adce5e538a7aacc670ec64c28d3f (diff) |
Documenting option 'Set Bracketing Last Introduction Pattern'.
Diffstat (limited to 'tools/coqdep.ml')
0 files changed, 0 insertions, 0 deletions