update comments

affeldt-aist · Jul 5, 2024 · 1990bc2 · 1990bc2
1 parent fdb3988
commit 1990bc2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/monad_model.v b/monad_model.v
@@ -1656,7 +1656,7 @@ HB.export ModelPlusArray.
                  f M <> fail :> M A.
       this would need parametricity axioms for its validation in a model.
    2. use syntactic reflection:
-      _ : forall (M : plusarraymonad) (m : M A),
+      _ : forall (M : plusArrayMonad) (m : M A),
           {S | evalArrayMonad S = m} -> m <> fail.
       here, S is an abstract syntax tree for a computation in MonadArray and
       evalArrayMonad is an evaluator that interprets S into a computation *)