cancel change to hierarchy.v

affeldt-aist · Jan 23, 2024 · 2212cbb · 2212cbb
1 parent 39056ec
commit 2212cbb
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/hierarchy.v b/hierarchy.v
@@ -1097,7 +1097,7 @@ HB.structure Definition ML_UNIVERSE := {ml_type & isML_universe ml_type}.
 Canonical isML_universe_eqType (T : ML_universe) := EqType T eqclass.
 
 HB.mixin Record isMonadTypedStore (MLU : ML_universe) (N : monad) (locT : eqType)
-    (M : UU0 -> UU0) of Monad M :={
+    (M : UU0 -> UU0) of Monad M := {
   cnew : forall {T : MLU}, coq_type N T -> M (loc locT T) ;
   cget : forall {T}, loc locT T -> M (coq_type N T) ;
   cput : forall {T}, loc locT T -> coq_type N T -> M unit ;