diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-29 15:22:34 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-29 15:22:34 -0700 |
| commit | 9f3c224e0bb968bebeca8f2d0d74e81517c6e293 (patch) | |
| tree | 60b8ce5c1f7321564d45d019bf69c763fe446d0f /src/Algebra.v | |
| parent | f729e58d23663c7bab0332e01e72e8c47ab5d8b3 (diff) | |
Don't generate goals [False] in conservative_common_denominator_all
See also #16, 4e50ef26b9b02c882536281e1c7a0cf013a963d5#r69034941">https://github.com/mit-plv/fiat-crypto/pull/16/files/f1744181ad236300cfa9ba7c033684fbdf45a3e9..4e50ef26b9b02c882536281e1c7a0cf013a963d5#r69034941
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 79b153352..771555cb0 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -770,10 +770,12 @@ Ltac set_nonfraction_pieces_by nonzero_tac := ltac:(fun T' => change T'); deduplicate_nonfraction_pieces mul end. +Ltac default_set_nonfraction_nonzero_tac := + try (intro; field_nonzero_mul_split; tauto). Ltac set_nonfraction_pieces_in H := - set_nonfraction_pieces_in_by H ltac:(try (intro; field_nonzero_mul_split; try tauto)). + set_nonfraction_pieces_in_by H default_set_nonfraction_nonzero_tac. Ltac set_nonfraction_pieces := - set_nonfraction_pieces_by ltac:(try (intro; field_nonzero_mul_split; tauto)). + set_nonfraction_pieces_by default_set_nonfraction_nonzero_tac. Ltac conservative_common_denominator_in H := idtac; let fld := guess_field in |