change the definition of MonadBr to match MonadTrigger

theories/Core/Utils.v

@@ -11,7 +11,7 @@ Polymorphic Class MonadTrigger (E : Type -> Type) (M : Type -> Type) : Type :=
   mtrigger : forall {X}, E X -> M X.
 
 Polymorphic Class MonadBr (B : Type -> Type) (M : Type -> Type) : Type :=
-  mbr : forall X (b: B X), M X.
+  mbr : forall {X}, B X -> M X.
 
 Polymorphic Class MonadStep (M : Type -> Type) : Type :=
   mstep : M unit.

theories/Interp/Fold.v

@@ -61,7 +61,7 @@ Definition interp {E B M : Type -> Type}
   {Mstep : MonadStep M}
   {Mbranch : MonadBr B M}
   (h : E ~> M) : ctree E B ~> M :=
-  fold h mbr.
+  fold h (@mbr B M Mbranch).
 
 Arguments interp {E B M FM MM IM _ _ _} h [T].
 

theories/Interp/FoldCTree.v

@@ -122,7 +122,7 @@ Section FoldCTree.
        | GuardF t => Guard (interp h t)
        | StepF  t => Step  (Guard (interp h t))
 	     | VisF e k => bind (h _ e) (fun x => Guard (interp h (k x)))
-	     | BrF c k => bind (mbr _ c) (fun x => Guard (interp h (k x)))
+	     | BrF c k => bind (mbr c) (fun x => Guard (interp h (k x)))
        end)%function.
 
     (** Unfold lemma. *)

theories/Interp/FoldStateT.v

@@ -33,7 +33,7 @@ Arguments fequ : simpl never.
 
 #[global] Instance MonadBr_stateT {S M C} {MM : Monad M} {AM : MonadBr C M}:
   MonadBr C (stateT S M) :=
-  fun X c s => f <- mbr _ c;; ret (s,f).
+  fun X c s => f <- mbr c;; ret (s,f).
 
 #[global] Instance MonadTrigger_stateT {E S M} {MM : Monad M} {MT: MonadTrigger E M} :
   MonadTrigger E (stateT S M) :=
@@ -225,7 +225,7 @@ Section State.
      | GuardF t => Guard (interp_state h t s)
      | StepF t => Step (Guard (interp_state h t s))
  	   | VisF e k => bind (h _ e s) (fun xs => Guard (interp_state h (k (snd xs)) (fst xs)))
-	   | BrF c k => bind (mbr (M := stateT _ _) _ c s) (fun xs => Guard (interp_state h (k (snd xs)) (fst xs)))
+	   | BrF c k => bind (mbr (M := stateT _ _) c s) (fun xs => Guard (interp_state h (k (snd xs)) (fst xs)))
      end)%function.
 
   Lemma unfold_interp_state `{C-<D} (t : ctree E C R) (s : S) :