aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-04 10:44:42 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-04 10:44:42 +0200
commit01128a2ff774f0ef249ee54a67e88d49ae254a4d (patch)
tree5b1dc69b34988ad1c60f8cadcb9233749c917876 /Makefile.doc
parentc2ceb06d88c63814dd704cd505420dc44841c026 (diff)
parent1d7fef8272d13a6e57bc46218d4a89c7e725c4d2 (diff)
Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension of List
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions