aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-09-01 09:38:32 +0000
committerGitHub2020-09-01 09:38:32 +0000
commit46768229c5349aa92a8107cd0a6ded32fd22d768 (patch)
tree1b2ab0b4ef712acb50c0e00bc04dfd9f42d874ae /printing/printer.ml
parentd66dbf1b6395454ea58621ef4eab5eb0b5f7fead (diff)
parentec23372744683b8d0b5dfa01eb731c33e73fef4e (diff)
Merge PR #12961: [declare] Return both declared constants in Derive path.
Reviewed-by: SkySkimmer
Diffstat (limited to 'printing/printer.ml')
0 files changed, 0 insertions, 0 deletions