aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto2/_CoqProject
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-06-18 14:32:58 +0200
committerPierre-Marie Pédrot2018-06-18 14:46:09 +0200
commit1bbeba35eb385f813a0e4b6d25a437f9bab8191b (patch)
tree654b722111fe371722b49c1f52a5ee0e2baf1e24 /doc/plugin_tutorial/tuto2/_CoqProject
parent1103a3f909b070a54d8fe2765b274aa7d217ec91 (diff)
Fixing a batch of deprecation warnings.
Diffstat (limited to 'doc/plugin_tutorial/tuto2/_CoqProject')
0 files changed, 0 insertions, 0 deletions