diff options
author | 2018-05-06 17:36:18 +0200 | |
---|---|---|
committer | 2018-05-08 01:10:55 +0200 | |
commit | 818ba539cf4a0aed2172f370dcddd380b6ec6a4c (patch) | |
tree | 4eddde38a39038139f4771adbcb0c8db8cf5d148 /pretyping/arguments_renaming.mli | |
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 'pretyping/arguments_renaming.mli')
0 files changed, 0 insertions, 0 deletions