diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-09 17:32:39 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-07-11 09:59:13 -0400 |
| commit | f736d37d0561a32e1201db10484a1c97d142a0c3 (patch) | |
| tree | ec23054dacfd52e45d2251eaa0ffc917a2628be3 | |
| parent | f5c1d1e55617000d79ef4bedb899f410f09d1e4f (diff) | |
rename [common_denominator] to [field_simplify_if_div]
| -rw-r--r-- | src/Algebra.v | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index f2c47b081..2ce0183ca 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -668,7 +668,7 @@ Ltac field_nonzero_mul_split := => apply IntegralDomain.mul_nonzero_nonzero_iff in H; destruct H end. -Ltac common_denominator := +Ltac field_simplify_eq_if_div := let fld := guess_field in lazymatch type of fld with field (div:=?div) => @@ -679,7 +679,7 @@ Ltac common_denominator := end. (** We jump through some hoops to ensure that the side-conditions come late *) -Ltac common_denominator_in_cycled_side_condition_order H := +Ltac field_simplify_eq_if_div_in_cycled_side_condition_order H := let fld := guess_field in lazymatch type of fld with field (div:=?div) => @@ -689,15 +689,11 @@ Ltac common_denominator_in_cycled_side_condition_order H := end end. -Ltac common_denominator_in H := +Ltac field_simplify_eq_if_div_in H := side_conditions_before_to_side_conditions_after - common_denominator_in_cycled_side_condition_order + field_simplify_eq_if_div_in_cycled_side_condition_order H. -Ltac common_denominator_all := - common_denominator; - repeat match goal with [H: _ |- _ _ _ ] => progress common_denominator_in H end. - (** Now we have more conservative versions that don't simplify non-division structure. *) Ltac deduplicate_nonfraction_pieces mul := repeat match goal with @@ -789,7 +785,7 @@ Ltac conservative_common_denominator_in H := lazymatch type of H with | appcontext[div] => set_nonfraction_pieces_in H; - common_denominator_in H; + field_simplify_eq_if_div_in H; [ | default_conservative_common_denominator_nonzero_tac.. ]; repeat match goal with H := _ |- _ => subst H end @@ -805,7 +801,7 @@ Ltac conservative_common_denominator := lazymatch goal with | |- appcontext[div] => set_nonfraction_pieces; - common_denominator; + field_simplify_eq_if_div; [ | default_conservative_common_denominator_nonzero_tac.. ]; repeat match goal with H := _ |- _ => subst H end |