diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-20 14:50:38 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-20 14:50:38 +0200 |
| commit | 011a2fe3ab6841d9c7ad700e6d298d5cffe72db5 (patch) | |
| tree | 9b71011ec3cb9aae309b32c3173579632efdc143 | |
| parent | 362ed8371062cea08ae2d7e5842091bf184393cb (diff) | |
| parent | 9051c1618062ce014719de5c3f73832e9a282a4d (diff) | |
Merge PR #899: [general] Move files to directories so they match linking order.
| -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 |