aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-24 14:14:22 +0100
committerGitHub2018-11-24 14:14:22 +0100
commitb8c4bf77c19670099b1fea44f3ab6204faa25d6b (patch)
tree631fc42f0e73fc8af5edb5aa77578f82b6edca20 /dev/include
parentc22494cd30ebfb705530176c322bb42219e2d422 (diff)
parentf05f4ebe9e91829e2817c63d90ec328f430992c4 (diff)
Merge pull request coq/ltac2#87 from ppedrot/camlp5-safe-api-strikes-back
Fix w.r.t. coq/coq#9051.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions