aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto2
diff options
context:
space:
mode:
authorSamuel Gruetter2021-03-23 15:59:48 -0400
committerSamuel Gruetter2021-03-23 15:59:48 -0400
commit1657b1156c29d969f1e8a1b5785e17d5984ea7a6 (patch)
treed6484337c5717ea00037d85a1edc31b46d7da40c /doc/plugin_tutorial/tuto2
parentd3f78cad1532f000106ed0c0b8be2ac384ce1d3a (diff)
fix documentation of Ltac2.Env.expand
Diffstat (limited to 'doc/plugin_tutorial/tuto2')
0 files changed, 0 insertions, 0 deletions