diff options
| author | Pierre-Marie Pédrot | 2019-05-11 15:35:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-11 17:36:03 +0200 |
| commit | 150fd1b6a50aff5e2476888eead3d33dc2f3d1fd (patch) | |
| tree | 5c6454933f18760203b0d568ba5601f45cc285f9 /kernel/nativelambda.mli | |
| parent | b83c29a099bde1ea71161c994bbf69b931e6d0f6 (diff) | |
Remove the elimrename field from Tactics.eliminator.
This is actually dead code, we never observe it.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions