diff options
| author | Pierre-Marie Pédrot | 2015-10-27 11:44:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-27 12:40:01 +0100 |
| commit | d51e5688f521c8a77a1dbdb0b88d8f99d5ff8060 (patch) | |
| tree | 3fa5d830feb50a5f96e07c6c4762ac8c3f461189 /dev | |
| parent | 73c3dddc94dda003b1bb854d3b6ca9d15474e299 (diff) | |
Finer type for Pcoq.interp_entry_name.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions