aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto0/src
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-04-05 09:40:46 +0200
committerGitHub2019-04-05 09:40:46 +0200
commitd47892548aebfb6640a8721ee1ec3493bfd3ce2a (patch)
tree8834c79b4efe2f2ccb516828956349ec2cb89f7d /doc/plugin_tutorial/tuto0/src
parentdc903c82c2308ae638147c5428511abe9279bf6d (diff)
parent0d8a4ec0f7486f47b7cff4cda465e2bd10c163ac (diff)
Merge pull request coq/ltac2#116 from proux01/master-parsing-decimal
[coq] Adapt to coq/coq#8764
Diffstat (limited to 'doc/plugin_tutorial/tuto0/src')
0 files changed, 0 insertions, 0 deletions