diff options
| author | Gaëtan Gilbert | 2019-10-29 13:27:25 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-12-16 11:48:53 +0100 |
| commit | 097796f1ebfa4009502e23494af08f332613ace3 (patch) | |
| tree | 8c484cca87b6a647804e3bc760932f284902373e /kernel/indTyping.ml | |
| parent | 62adf2b9e03afa212fcd8819226da068bf4a32b8 (diff) | |
comInductive: remove redundant check_evars calls
We do [solve_remaining_evars all_and_fail_flags] immediately before
calling [interp_mutual_inductive_constr] so these checks are extra.
Diffstat (limited to 'kernel/indTyping.ml')
0 files changed, 0 insertions, 0 deletions