aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-15 18:17:04 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-15 18:17:04 +0100
commitd7691de7184b4cdcfd48fd762011569cde5523c5 (patch)
tree9c9e14226b070fc2a5cf4c216c4f8c634de20855 /tools/coqdep.ml
parenteed12bddc3e6f6f9192c909a8b8f82859080f3a1 (diff)
parentaed3c876d422f4dcc0296fd4949148c697f37b1d (diff)
Merge branch 'v8.5'
Diffstat (limited to 'tools/coqdep.ml')
0 files changed, 0 insertions, 0 deletions