From 871a43641231f8127b04c85bb75437de9b4dec72 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 27 Feb 2026 14:12:08 +0100 Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21611 --- src/freeg.v | 2 +- src/monalg.v | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/freeg.v b/src/freeg.v index a116fe7..3a88df6 100644 --- a/src/freeg.v +++ b/src/freeg.v @@ -92,7 +92,7 @@ Module FreegDefs. Canonical prefreeg_equiv_direct := defaultEncModRel equiv. Definition type := {eq_quot equiv}. - Definition type_of of phant G & phant K := type. + Definition type_of & phant G & phant K := type. Notation "{ 'freeg' K / G }" := (type_of (Phant G) (Phant K)). diff --git a/src/monalg.v b/src/monalg.v index 5ed67e6..b9375f1 100644 --- a/src/monalg.v +++ b/src/monalg.v @@ -52,7 +52,7 @@ Reserved Notation "'{' 'mmorphism' M '->' S '}'" (M at level 98, format "{ 'mmorphism' M -> S }"). (* -------------------------------------------------------------------- *) -HB.mixin Record Choice_isMonomialDef V of Choice V := { +HB.mixin Record Choice_isMonomialDef V & Choice V := { one : V; mul : V -> V -> V; mulmA : associative mul; @@ -77,7 +77,7 @@ Local Notation "*%M" := (@mmul _) : function_scope. Local Notation "x * y" := (mmul x y) : monom_scope. (* -------------------------------------------------------------------- *) -HB.mixin Record MonomialDef_isConomialDef V of MonomialDef V := { +HB.mixin Record MonomialDef_isConomialDef V & MonomialDef V := { mulmC : commutative (@mul V) }.