diff options
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 6 | ||||
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 01018c3e2..6eeee9f48 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -232,7 +232,7 @@ Module Ring. Lemma Good : GoodT. Proof. - split_and. + split_and; simpl in *. repeat match goal with | [ H : context[andb _ true] |- _ ] => setoid_rewrite andb_true_r in H end. @@ -441,7 +441,7 @@ Module MontgomeryStyleRing. Qed. Lemma Good : GoodT. Proof. - split_and. + split_and; simpl in *. repeat match goal with | [ H : context[andb _ true] |- _ ] => setoid_rewrite andb_true_r in H end. @@ -839,7 +839,7 @@ Module Pipeline. | _ => eassumption || reflexivity end.. ]. { subst; split; [ | assumption ]. - split_and. + split_and; simpl in *. split; [ solve [ eauto with nocore ] | ]. { intros; match goal with H : _ |- _ => erewrite H; clear H end; eauto. transitivity (type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds e arg_bounds)) arg1). diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index abbf08a05..92799222e 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -2173,7 +2173,7 @@ Module Ring. Lemma Good : GoodT. Proof. - split_and. + split_and; simpl in *. eapply subsetoid_ring_by_ring_isomorphism; cbv [ring_opp ring_add ring_sub ring_mul ring_encode F.sub] in *; repeat match goal with |