diff options
| author | Gaëtan Gilbert | 2018-09-11 23:17:28 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-19 13:15:24 +0200 |
| commit | 11a748d42dbf8536abceccbedc350806fcdab8eb (patch) | |
| tree | c890774f2dd6a74ce926d6cc6f8c66a80f0f2f3d /engine/eConstr.ml | |
| parent | 6d74efabf11768ca1df3a2f3d5a65d25f7f95b01 (diff) | |
Remove Hints.add_hints_init
It was only used in ltac/rewrite which as a plugin is too late to
affect init.
Diffstat (limited to 'engine/eConstr.ml')
0 files changed, 0 insertions, 0 deletions