diff options
| author | Pierre-Marie Pédrot | 2017-07-21 14:49:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-01 16:11:55 +0200 |
| commit | cabce8ae233040c2365bfd8bd1f478676fcade33 (patch) | |
| tree | 92bd7153a50e16ed98ceda7a70489df7f8a97ba3 /kernel/type_errors.ml | |
| parent | 65bd1deac80689d02be7ef580872974cc38bf93c (diff) | |
Detyping functions are now operating on EConstr.t.
This was already the case, but the API was not exposing this.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions