diff options
| author | Emilio Jesus Gallego Arias | 2018-05-06 17:36:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-08 01:10:55 +0200 |
| commit | 818ba539cf4a0aed2172f370dcddd380b6ec6a4c (patch) | |
| tree | 4eddde38a39038139f4771adbcb0c8db8cf5d148 /dev | |
| parent | 0b6f9dafdd828466ab87306f30f3aae0bc689f4f (diff) | |
[CoqProject] Add some comments and remove unnecessary use of Pp.
But indeed we need to split this file, as it is used now from CoqIDE
is incorrect.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions