diff options
| author | Emilio Jesus Gallego Arias | 2017-07-13 19:53:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 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 154793a32d..154793a32d 100644 --- a/library/declare.ml +++ b/interp/declare.ml diff --git a/library/declare.mli b/interp/declare.mli index 6a09434645..6a09434645 100644 --- a/library/declare.mli +++ b/interp/declare.mli diff --git a/library/impargs.ml b/interp/impargs.ml index b7125fc85d..b7125fc85d 100644 --- a/library/impargs.ml +++ b/interp/impargs.ml diff --git a/library/impargs.mli b/interp/impargs.mli index 4b78f54eac..4b78f54eac 100644 --- a/library/impargs.mli +++ b/interp/impargs.mli diff --git a/printing/miscprint.ml b/proofs/miscprint.ml index 5d37c8a024..5d37c8a024 100644 --- a/printing/miscprint.ml +++ b/proofs/miscprint.ml diff --git a/printing/miscprint.mli b/proofs/miscprint.mli index 21d410c7b0..21d410c7b0 100644 --- a/printing/miscprint.mli +++ b/proofs/miscprint.mli diff --git a/vernac/ind_tables.ml b/tactics/ind_tables.ml index 0407c1e36a..0407c1e36a 100644 --- a/vernac/ind_tables.ml +++ b/tactics/ind_tables.ml diff --git a/vernac/ind_tables.mli b/tactics/ind_tables.mli index 005555caa0..005555caa0 100644 --- a/vernac/ind_tables.mli +++ b/tactics/ind_tables.mli |