diff options
| author | Maxime Dénès | 2017-07-20 14:50:38 +0200 |
|---|---|---|
| committer | Maxime Dénès | 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 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 |