diff options
Diffstat (limited to 'src/Experiments/NewPipeline/Toplevel1.v')
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 6 |
1 files changed, 3 insertions, 3 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). |