mathlib3
refactor(*): drop `lattice` namespace
#2166
Merged

refactor(*): drop `lattice` namespace #2166

mergify merged 9 commits into master from lattice-ns
urkud
urkud refactor(*): drop `lattice` namespace
26b29a1a
urkud Fix some compile failures
26636fd2
urkud Fix the rest of compile failures
67a00871
ChrisHughes24
urkud
urkud urkud added awaiting-review
cipher1024 cipher1024 assigned ChrisHughes24 ChrisHughes24 5 years ago
cipher1024
urkud
ChrisHughes24
ChrisHughes24 Merge remote-tracking branch 'origin/master' into HEAD
35a9c660
ChrisHughes24 ChrisHughes24 added ready-to-merge
ChrisHughes24 ChrisHughes24 removed awaiting-review
ChrisHughes24 Merge remote-tracking branch 'origin/master' into HEAD
efc0fa85
ChrisHughes24 fix build
8a08725a
ChrisHughes24 fix build
15d7cf19
urkud Fix build
3b7c4597
sgouezel
sgouezel approved these changes on 2020-03-19
mergify[bot] Merge branch 'master' into lattice-ns
f25b4233
mergify mergify merged 9dbc6069 into master 5 years ago
mergify mergify deleted the lattice-ns branch 5 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
Labels
Milestone