diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-21 14:49:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-01 16:11:55 +0200 |
| commit | cabce8ae233040c2365bfd8bd1f478676fcade33 (patch) | |
| tree | 92bd7153a50e16ed98ceda7a70489df7f8a97ba3 /plugins/quote | |
| 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 'plugins/quote')
0 files changed, 0 insertions, 0 deletions