diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-02-06 18:25:31 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | d641525010b941607605b7e998b53ba6d99783e5 (patch) | |
| tree | c8678c172d8b7ae27ae660fe40b7b73a51c64ba1 /src/Algebra.v | |
| parent | 255ce6372b3d3a6ca40e8dbddbf955047232a8e6 (diff) | |
field_nsatz
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index e126fd9af..c9e535dd5 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1262,7 +1262,7 @@ Ltac _field_nsatz_prep_inequalities fld eq zero := Ltac field_nsatz := let fld := guess_field in let eq := match type of fld with field(eq:=?eq) => eq end in - let zero := match type of fld with field(zero:=?zero) => eq end in + let zero := match type of fld with field(zero:=?zero) => zero end in _field_nsatz_prep_goal fld eq; common_denominator_equality_inequality_all; [|_field_nsatz_prep_goal fld eq..]; _field_nsatz_prep_inequalities fld eq zero; |