diff options
| author | Pierre-Marie Pédrot | 2020-12-12 14:39:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-12 14:46:45 +0100 |
| commit | 421ed6bb43e01a2675df2cfae286d1cfcc691fcc (patch) | |
| tree | 3bc425e990ecb93f1a9ac5e428466ef75cf1fd1e /kernel | |
| parent | 12d53dc64fa565ae6408d2ebb668e997b7e574b3 (diff) | |
Small API encapsulation inside Redexpr.
We move bind_red_expr_occurrences from Tactics to Redexpr, where it
semantically belongs. We also hide it and seal the corresponding evaluated
types.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions