From 8fb51cd75397908077532442959ab412c41f6ea0 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 29 Jul 2024 12:06:11 +0200 Subject: [PATCH] Fix compilation with Coq master --- refinements/poly_div.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/refinements/poly_div.v b/refinements/poly_div.v index 21c4857..8c9bb61 100644 --- a/refinements/poly_div.v +++ b/refinements/poly_div.v @@ -169,10 +169,8 @@ Qed. (scal_poly (N:=nat) (R:=R) (polyR:={poly R})) (scal_poly (N:=N) (R:=C) (polyR:=polyC)). Proof. - rewrite refinesE=> p p' hp q q' hq. - eapply (scal_poly_R (polyR_R:=RpolyC))=> // *; - eapply refinesP; - do ?eapply refines_apply; tc. + apply: refines_abstr2 => p p' hp q q' hq; rewrite refinesE. + by apply: (scal_poly_R (R_R:=rC) (polyR_R:=RpolyC)) => *; apply: refinesP. Qed. #[export] Instance refine_scal_poly :