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