Fix monad_map_branches_k name (#953)

MetaCoq · Oct 16, 2023 · 3020c10 · 3020c10
1 parent 1fcd7ff
commit 3020c10
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/pcuic/theories/PCUICMonadAst.v b/pcuic/theories/PCUICMonadAst.v
@@ -59,6 +59,6 @@ Section with_monad.
   Definition monad_map_branch_k {term term'} (f : nat -> term -> T term') g k b
     := @monad_map_branch term term' (f (#|bcontext b| + k)) g b.
 
-  Notation map_branches_k f h k brs :=
-    (monad_map (monad_map_branch_k f h k) brs).
+  Definition monad_map_branches_k {term term'} f h k brs :=
+    (monad_map (@monad_map_branch_k term term' f h k) brs).
 End with_monad.
diff --git a/template-coq/theories/MonadAst.v b/template-coq/theories/MonadAst.v
@@ -62,6 +62,6 @@ Section with_monad.
 
   Definition monad_map_branches {term B} (f : term -> T B) l := monad_map (monad_map_branch f) l.
 
-  Notation monad_map_branches_k f k brs :=
-    (monad_map (fun b => monad_map_branch (f (#|b.(bcontext)| + k)) b) brs).
+  Definition monad_map_branches_k {term term'} f k brs :=
+    (monad_map (fun b => @monad_map_branch term term' (f (#|b.(bcontext)| + k)) b) brs).
 End with_monad.