diff options
| author | Pierre-Marie Pédrot | 2019-05-11 17:38:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-14 15:51:48 +0200 |
| commit | 695990d2929e4026d13ec2acd95b3647c7bcc6e7 (patch) | |
| tree | 8584eada9dd2dbce5b8fa1ce4ef1eaf8792bfbd1 /kernel/type_errors.ml | |
| parent | cc1d9256b721b859d7a0dbe63a991f3e40aa67d3 (diff) | |
Remove the sidecond_first flag of apply-related tactics.
This was dead code.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions