Merge pull request #91 from proux01/coq_master

Fix compilation with Coq master
coq-community · Jul 29, 2024 · 86bb4c9 · 86bb4c9
2 parents b974778 + 8fb51cd
commit 86bb4c9
Showing 1 changed file with 2 additions and 4 deletions.
diff --git 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 :