diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-31 10:52:13 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-31 10:52:13 +0200 |
| commit | 22db6304ffd45d7ae6e4a0acf909afb1ec55d02c (patch) | |
| tree | 7c8a970f1f6c4712223ad9ee366783e89576e5e0 /vernac/vernacstate.mli | |
| parent | 4598a26890a896ddcf6cd30758ae07882e245a16 (diff) | |
| parent | 8b302bfba8f98458087685c8d5fbca2cf647255f (diff) | |
Merge PR #7564: Move interning the [hint_pattern] outside the Typeclasses hooks.
Diffstat (limited to 'vernac/vernacstate.mli')
0 files changed, 0 insertions, 0 deletions