diff options
| author | Pierre-Marie Pédrot | 2020-01-29 15:57:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-29 15:57:36 +0100 |
| commit | 8c04d108e1f57d0e8e11483a7c9de721ab2f026a (patch) | |
| tree | 28d83c15993beecdc50cfb990c1c4646cc47b623 /kernel/type_errors.mli | |
| parent | c8aac351b7e0e9c98238eecbe2d8cf3c6f917373 (diff) | |
| parent | 72201ba9afb95ed0bfdd9e9e2cdeb089b7224a76 (diff) | |
Merge PR #11399: Checker: use inductive's check_template flag
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions