aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto2/src
diff options
context:
space:
mode:
authorSamuel Gruetter2021-04-07 21:02:10 -0400
committerSamuel Gruetter2021-04-07 21:02:10 -0400
commitfb63ec7c10076d156caa43f73bad4f69653862a6 (patch)
tree8311e352a1556d7b876ea1cbdde87ce538c7f9a7 /doc/plugin_tutorial/tuto2/src
parent59d0462f35818c12a0727a560d7b9ecf2ceea994 (diff)
unify for Ltac2
Fixes #14083
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src')
0 files changed, 0 insertions, 0 deletions