diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-17 13:45:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-19 01:17:39 +0100 |
| commit | 805c8987fbb5fdeb94838bb5a3a7364c0a3d3374 (patch) | |
| tree | 847bc8e25c550394991eee31aba854667f0b60e7 /pretyping/evarconv.mli | |
| parent | a99aa093b962e228817066d00f7e12698f8df73a (diff) | |
Do not export entry_key from Pcoq anymore.
Diffstat (limited to 'pretyping/evarconv.mli')
0 files changed, 0 insertions, 0 deletions