aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2021-03-10 13:57:38 +0100
committerPierre-Marie Pédrot2021-03-16 20:02:56 +0100
commit2915154835b8d0a90a5c3ca79c37d66142dc9a33 (patch)
treeb653e3878452bc2a63dd76d7afcfc6760bdf19d7 /doc/stdlib
parent17b5c56ab72d42f3cf71390e0f9beed360c9777f (diff)
Add tests for the new Ltac2 Ind API.
Diffstat (limited to 'doc/stdlib')
0 files changed, 0 insertions, 0 deletions