diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-03-02 10:58:28 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | 0ab98d3380033b58162015656f435ae90b936856 (patch) | |
| tree | 38a17503ccbc5fd51d473f458e782812360ed5b1 /src/Algebra/Field.v | |
| parent | 7f0ba34481f59db0cf430d7a08b8b65d953eb803 (diff) | |
make 8.5 happy
Diffstat (limited to 'src/Algebra/Field.v')
| -rw-r--r-- | src/Algebra/Field.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v index e901bde2f..76b2a9ed3 100644 --- a/src/Algebra/Field.v +++ b/src/Algebra/Field.v @@ -271,7 +271,7 @@ Ltac _inverse_to_equation_by fld d tac := lazymatch goal with | H: eq (mul ?di d) one |- _ => rewrite <-!(left_inv_unique(H:=fld) _ _ H) in * | H: eq (mul d ?di) one |- _ => rewrite <-!(right_inv_unique(H:=fld) _ _ H) in * - | _ => _introduce_inverse constr:(fld) constr:(d) d_nz + | _ => _introduce_inverse fld d d_nz end; clear d_nz. |