aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-07 13:54:19 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-07 13:54:19 +0200
commitfe371675fc85d712f5124d73157bd833e8fa14a6 (patch)
tree016f5957e12443578c2806b619fc7a22bcf31518 /vernac
parent49a587ec6e6a792bb246dffe16b6fe70bc47897e (diff)
parent26643cdd013f5df2bcae099852932ac09e93f8fb (diff)
Merge PR #8005: Fix compilation of Coq with camlp5 master branch.
Diffstat (limited to 'vernac')
0 files changed, 0 insertions, 0 deletions