aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/solvable
diff options
context:
space:
mode:
authorErik Martin-Dorel2019-02-27 17:31:35 +0100
committerErik Martin-Dorel2019-03-20 12:54:26 +0100
commitc07f1f8d89dd1f975e06e8c45df2c7a4e6ca7fc3 (patch)
tree73c109057bf3f18127be887fcc1b2e0ba82ff3e2 /mathcomp/solvable
parent4c8455594c5adff08761037a5919c058d0d502ba (diff)
Add extra eta lemmas for the under tactic
Related: coq/coq#9651
Diffstat (limited to 'mathcomp/solvable')
0 files changed, 0 insertions, 0 deletions