diff options
| author | Emilio Jesus Gallego Arias | 2018-05-06 16:57:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-08 01:10:55 +0200 |
| commit | 0b6f9dafdd828466ab87306f30f3aae0bc689f4f (patch) | |
| tree | a49004a54f6f5cd9af54ca630cc16016be4f6161 /dev | |
| parent | 2c52a8304ed2bab9fc110818160463f57ba8fccd (diff) | |
[coqdep] Remove unnecessary dependency on Pp and CError.
This allows for even earlier bootstrapping.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions