aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorInModule.v
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2021-01-21 15:16:30 +0100
committerPierre-Marie Pédrot2021-03-10 12:23:41 +0100
commite976e2cc4ad8fd361aa54b071543f75dbb532ccd (patch)
treea602d5b5331a107230eeb41b9459315655302416 /test-suite/output/ErrorInModule.v
parente16a73156d92a6510e34e54a829f43f294820646 (diff)
Allow to register deprecation status in Ltac2 term and notation declarations.
Diffstat (limited to 'test-suite/output/ErrorInModule.v')
0 files changed, 0 insertions, 0 deletions