aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorEmilio Jesús Gallego Arias2018-12-05 17:48:44 +0100
committerGitHub2018-12-05 17:48:44 +0100
commit707c99ce29fdca3c02c0ea573d1bf20490f361f2 (patch)
tree19f86f4660aaa697199a27cecc64e85b082d2d92 /doc
parentb5ebc0a2aa4e73054b6085dd82211a08636c1418 (diff)
parentdf40307f70d7a03b03af7ae4360a15349abc1bd0 (diff)
Merge pull request #20 from ejgallego/vernac+remove_empty_hooks
[coq overlay] Adapt to coq/coq#8705
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions