aboutsummaryrefslogtreecommitdiff
path: root/.github/pull_request_template.md
diff options
context:
space:
mode:
authorCyril Cohen2020-05-04 13:16:47 +0200
committerGitHub2020-05-04 13:16:47 +0200
commit582a4a3943652b1ba7e9e689bf4051ada17f1c36 (patch)
tree43a6e64af7d1850e409fb070013eef1113937a76 /.github/pull_request_template.md
parent9ecb541cd573534a3144dd5b5f86c4312ff798b5 (diff)
parent3548a49db7f9ddc181a27ba0762686b2f2aee30c (diff)
Merge pull request #493 from pi8027/rm-tuple-lemmas-in-order
Remove the tuple extensions in order.v that is available in tuple.v
Diffstat (limited to '.github/pull_request_template.md')
0 files changed, 0 insertions, 0 deletions