aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-02-07 12:29:39 +0100
committerGaëtan Gilbert2019-02-12 17:16:39 +0100
commit7104904f9f6e1a5e1b1590bd898ae20cb7178daf (patch)
tree7096fac4343b585e9fd168ce753d53ae8f0cdd1e /dev/include
parent75269e1b3fb98c8095b7f50e8ade2af87eb4061f (diff)
Fix failing coqtops universe-polymorphism.rst
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions