diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-08 20:01:09 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-08 20:04:53 -0500 |
| commit | 09ba899b557b734749fa8247952ffcb7209e44f6 (patch) | |
| tree | 2afe6ddc12ddd5eb00c7f9b1e9fa526edcc0ea5a /src | |
| parent | 0f72cd3556f22fa815f692e5608d6539d447baea (diff) | |
Fix f_equiv brokenness in 8.4, even faster src/MxDHRepChange.v
Diffstat (limited to 'src')
| -rw-r--r-- | src/MxDHRepChange.v | 24 |
1 files changed, 10 insertions, 14 deletions
diff --git a/src/MxDHRepChange.v b/src/MxDHRepChange.v index d0ef046ca..4596ad188 100644 --- a/src/MxDHRepChange.v +++ b/src/MxDHRepChange.v @@ -23,20 +23,14 @@ Section MxDHRepChange. Qed. Ltac t := + let hom := match goal with H : is_homomorphism |- _ => H end in + let mhom := constr:(@homomorphism_is_homomorphism _ _ _ _ _ _ _ _ _ _ _ hom) in repeat ( - (let hom := match goal with H : Monoid.is_homomorphism |- _ => H end in - repeat ( - rewrite (@homomorphism_id _ _ _ _ _ _ _ _ _ _ _ _ _ hom) - ) - ) || - (let hom := match goal with H : is_homomorphism |- _ => H end in - repeat ( - rewrite (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ hom) || - rewrite (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ hom) || - rewrite (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ hom) || - rewrite (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ hom) - ) - ) || + rewrite (@homomorphism_id _ _ _ _ _ _ _ _ _ _ _ _ _ mhom) || + rewrite (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ hom) || + rewrite (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ hom) || + rewrite (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ hom) || + rewrite (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ hom) || rewrite homomorphism_a24 || rewrite homomorphism_multiplicative_inverse_complete' || reflexivity @@ -106,7 +100,9 @@ Section MxDHRepChange. generalize dependent init; generalize dependent init'. induction xs; [solve [eauto]|]. repeat intro; simpl; rewrite IHxs by eauto. - f_equiv; eapply Proper_step'; eauto. + apply (_ : Proper ((R ==> eq ==> R) ==> SetoidList.eqlistA eq ==> R ==> R) (@fold_left _ _)); + try reflexivity; + eapply Proper_step'; eauto. Qed. Global Instance Proper_downto {T R} {Equivalence_R:@Equivalence T R} : |