mathlib3
chore(tactic/transport): rename to transform_decl
#2308

Merged

chore(tactic/transport): rename to transform_decl #2308

mergify merged 5 commits into master from rename-transport

chore(tactic/transport): rename to transform_decl

59203835

bryangingechen approved these changes on 2020-04-01

bryangingechen added ready-to-merge

satisfying the linter

05708a26

oops, wrong comment format

812ecacb

Merge branch 'master' into rename-transport

c0447f29

Merge branch 'master' into rename-transport

ba15a12c

mergify merged 33764abc into master 6 years ago

mergify deleted the rename-transport branch 6 years ago

Reviewers

bryangingechen

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone