From e38db3a74c1960374da2105987aa999e45808fde Mon Sep 17 00:00:00 2001 From: Avi Shinnar Date: Mon, 2 Dec 2024 05:56:58 -0500 Subject: [PATCH] fix breakage from previous commit removing an unneeded hypothesis from a lemma Signed-off-by: Avi Shinnar --- coq/QLearn/qlearn_redux.v | 2 -- 1 file changed, 2 deletions(-) diff --git a/coq/QLearn/qlearn_redux.v b/coq/QLearn/qlearn_redux.v index 75ff8fab..2c0a87f1 100644 --- a/coq/QLearn/qlearn_redux.v +++ b/coq/QLearn/qlearn_redux.v @@ -2296,7 +2296,6 @@ Proof. (g := const (Rbar.Finite A2)). - typeclasses eauto. - typeclasses eauto. - - typeclasses eauto. - revert alpha_sqr. apply almost_impl, all_almost. intros; red; intros. @@ -2326,7 +2325,6 @@ Proof. (g := const (Rbar.Finite A2)). - typeclasses eauto. - typeclasses eauto. - - typeclasses eauto. - revert alpha_sqr. apply almost_impl, all_almost. intros; red; intros.