diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 09:38:18 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 09:38:18 +0100 |
| commit | 3da76841125ef48889c8eceb134116e2d0bd7a2e (patch) | |
| tree | 8728b456dab71560379044459e7a7c979a1b252b /plugins/ltac/tacinterp.ml | |
| parent | 0168ee0b6463a9ef44d768b0020b34785986c1cb (diff) | |
| parent | 1172b52735a299dfc91aee36b30b576dfeff581c (diff) | |
Merge PR #6419: [vernac] Split `command.ml` into separate files.
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
0 files changed, 0 insertions, 0 deletions