aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-18 09:38:18 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-18 09:38:18 +0100
commit3da76841125ef48889c8eceb134116e2d0bd7a2e (patch)
tree8728b456dab71560379044459e7a7c979a1b252b /proofs
parent0168ee0b6463a9ef44d768b0020b34785986c1cb (diff)
parent1172b52735a299dfc91aee36b30b576dfeff581c (diff)
Merge PR #6419: [vernac] Split `command.ml` into separate files.
Diffstat (limited to 'proofs')
0 files changed, 0 insertions, 0 deletions