diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-26 15:19:13 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-26 15:19:19 -0400 |
| commit | ce053effff183cbe61de6dd1e0261e596f73130e (patch) | |
| tree | 5a92c1cc02b3e75a43a79d767f08e3be13427d2e /src/Algebra.v | |
| parent | f493947f6296911c58e55b0dd23a158804b222c2 (diff) | |
Fix a missing case in generalize_inv
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index bd746d1b6..88b67ed07 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1257,6 +1257,8 @@ Ltac generalize_inv inv := repeat match goal with | [ |- context[inv ?x] ] => pose proof (lem x); generalize dependent (inv x); intros + | [ H : context[inv ?x] |- _ ] + => pose proof (lem x); generalize dependent (inv x); intros end. Ltac nsatz_strip_fractions_on inv := rewrite_field_div_definition inv; generalize_inv inv; specialize_by_assumption. |