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 /dev | |
| parent | 0168ee0b6463a9ef44d768b0020b34785986c1cb (diff) | |
| parent | 1172b52735a299dfc91aee36b30b576dfeff581c (diff) | |
Merge PR #6419: [vernac] Split `command.ml` into separate files.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index 1da5e3ed1..d7059fe74 100644 --- a/dev/base_include +++ b/dev/base_include @@ -170,7 +170,7 @@ open Eqschemes open ExplainErr open Class -open Command +open ComDefinition open Indschemes open Ind_tables open Auto_ind_decl |