mathlib3
fix(order.basic|ring_theory.algebra): lower instance priority
#1729

Merged

fix(order.basic|ring_theory.algebra): lower instance priority #1729

mergify merged 10 commits into master from instance_priority2

fpvandoorn added blocked-by-other-PR

robertylewis removed blocked-by-other-PR

robertylewis added WIP

fpvandoorn force pushed from 67dee04e to d1b0e469 6 years ago

algebra

69ecc4a2

algebra2

6df4c5ce

algebra3

d991a4ef

algebra4

e6867b2b

order.basic

53d9c7bb

module

67de0435

algebra/ring

83c7c22d

fpvandoorn force pushed from d1b0e469 to 83c7c22d 6 years ago

explain default priority of 100

60cb512e

undo priority changes

b8432383

robertylewis approved these changes on 2019-12-04

fpvandoorn removed WIP

fpvandoorn added ready-to-merge

Merge branch 'master' into instance_priority2

174b51a3

mergify merged d4ee5b69 into master 6 years ago

mergify deleted the instance_priority2 branch 6 years ago

Reviewers

robertylewis

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone