diff options
| author | Pierre-Marie Pédrot | 2018-07-26 11:06:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-26 11:06:23 +0200 |
| commit | b13c954c49f546ecbbc5f73d32e69348408e2ad4 (patch) | |
| tree | 95b3ba6a60246b511109951736e7f6bdb769e359 /kernel/declarations.ml | |
| parent | 3f6383c4042390b05651d20f04d4405589ffd8f3 (diff) | |
| parent | f2c59e19205eedc7d35f254b87a3acc457a8c36a (diff) | |
Merge PR #7786: In "redundant clause" pattern-matching error, show also the pattern (closes #7777)
Diffstat (limited to 'kernel/declarations.ml')
0 files changed, 0 insertions, 0 deletions