diff options
| author | Pierre-Marie Pédrot | 2015-06-30 16:47:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-06-30 16:49:15 +0200 |
| commit | 72f128af5a00e5509239e46b395c9cd10e53b36a (patch) | |
| tree | f0b9aecae361704b534abf45ebc63a1cabd5c3fb /kernel/type_errors.ml | |
| parent | 2defd4c15467736b73f69adb501e3a4fe2111ce5 (diff) | |
Removing dead code in coqdep.
Since commit 2f521670fbd, the Require "file" syntax was not used anymore by
coqtop but the code handling it was still there in coqdep. We finish the work
by erasing the remnant code.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions