diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-13 19:53:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-19 16:00:30 +0200 |
| commit | 9051c1618062ce014719de5c3f73832e9a282a4d (patch) | |
| tree | 9197008d190e21f99dbaf08967d57f8ebd43c8ce | |
| parent | e273ff57ef82e81ab6b6309584a7d496ae4659c1 (diff) | |
[general] Move files to directories matching linking order.
We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`,
`Miscprint`) to their proper place as they were declared in different
`mllib` files than the one in their directory.
In some cases this could be refined but we don't do anything fancy, we
just reflect the status quo.
| -rw-r--r-- | interp/declare.ml (renamed from library/declare.ml) | 0 | ||||
| -rw-r--r-- | interp/declare.mli (renamed from library/declare.mli) | 0 | ||||
| -rw-r--r-- | interp/impargs.ml (renamed from library/impargs.ml) | 0 | ||||
| -rw-r--r-- | interp/impargs.mli (renamed from library/impargs.mli) | 0 | ||||
| -rw-r--r-- | proofs/miscprint.ml (renamed from printing/miscprint.ml) | 0 | ||||
| -rw-r--r-- | proofs/miscprint.mli (renamed from printing/miscprint.mli) | 0 | ||||
| -rw-r--r-- | tactics/ind_tables.ml (renamed from vernac/ind_tables.ml) | 0 | ||||
| -rw-r--r-- | tactics/ind_tables.mli (renamed from vernac/ind_tables.mli) | 0 |
8 files changed, 0 insertions, 0 deletions
diff --git a/library/declare.ml b/interp/declare.ml index 154793a32..154793a32 100644 --- a/library/declare.ml +++ b/interp/declare.ml diff --git a/library/declare.mli b/interp/declare.mli index 6a0943464..6a0943464 100644 --- a/library/declare.mli +++ b/interp/declare.mli diff --git a/library/impargs.ml b/interp/impargs.ml index b7125fc85..b7125fc85 100644 --- a/library/impargs.ml +++ b/interp/impargs.ml diff --git a/library/impargs.mli b/interp/impargs.mli index 4b78f54ea..4b78f54ea 100644 --- a/library/impargs.mli +++ b/interp/impargs.mli diff --git a/printing/miscprint.ml b/proofs/miscprint.ml index 5d37c8a02..5d37c8a02 100644 --- a/printing/miscprint.ml +++ b/proofs/miscprint.ml diff --git a/printing/miscprint.mli b/proofs/miscprint.mli index 21d410c7b..21d410c7b 100644 --- a/printing/miscprint.mli +++ b/proofs/miscprint.mli diff --git a/vernac/ind_tables.ml b/tactics/ind_tables.ml index 0407c1e36..0407c1e36 100644 --- a/vernac/ind_tables.ml +++ b/tactics/ind_tables.ml diff --git a/vernac/ind_tables.mli b/tactics/ind_tables.mli index 005555caa..005555caa 100644 --- a/vernac/ind_tables.mli +++ b/tactics/ind_tables.mli |