diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-17 03:26:55 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-09 15:19:41 +0200 |
| commit | ca2a3bcf10cb8662751c7fcc5c58cd34196ecc9b (patch) | |
| tree | e196ebacba4fffa3a52a66b56a900ce4a78470d4 | |
| parent | f1598b00219a951e94036cb7f48a8fe1309025f1 (diff) | |
[deps] Move `Discharge` to `interp`
More dependencies / linking fixes.
| -rw-r--r-- | interp/discharge.ml (renamed from vernac/discharge.ml) | 0 | ||||
| -rw-r--r-- | interp/discharge.mli (renamed from vernac/discharge.mli) | 0 |
2 files changed, 0 insertions, 0 deletions
diff --git a/vernac/discharge.ml b/interp/discharge.ml index 0e4bbd299..0e4bbd299 100644 --- a/vernac/discharge.ml +++ b/interp/discharge.ml diff --git a/vernac/discharge.mli b/interp/discharge.mli index c8c7e3b8b..c8c7e3b8b 100644 --- a/vernac/discharge.mli +++ b/interp/discharge.mli |