diff options
| author | Emilio Jesus Gallego Arias | 2018-10-10 23:35:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-11 22:52:32 +0200 |
| commit | c8883873426c92778a1cac02da17e3d123beb394 (patch) | |
| tree | 9ffcf82e3787d11c447851dd850ec1cdd4d3611d /kernel/type_errors.ml | |
| parent | 27fd525445e8ab37e67eebfb2bca1963e33c7f64 (diff) | |
[vernac] Remove unused abstraction from declaration_hook type.
"Declaration" hooks can be polymorphic on their return type, however
this facility doesn't seem used in the codebase.
We thus remove the polymorphism with the hope to be able to reify the
control later on.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions