remove unnecessary annotations (#137)

* remove unnecessary annotations * put back annotation for clarity * use UU0
affeldt-aist · Jul 10, 2024 · 500baea · 500baea
1 parent b0798ad
commit 500baea
Showing 1 changed file with 3 additions and 4 deletions.
diff --git a/monad_model.v b/monad_model.v
@@ -1749,8 +1749,7 @@ Local Notation ml_type := (MLU : Type).
 Record binding :=
   mkbind { bind_type : ml_type; bind_val : coq_type bind_type }.
 
-Definition acto : UU0 -> UU0 :=
-  MS (seq binding) [the monad of option_monad].
+Definition acto : UU0 -> UU0 := MS (seq binding) option_monad.
 Local Notation M := acto.
 
 Definition def : binding := mkbind (val_nonempty N).
@@ -1761,7 +1760,7 @@ Notation loc := (@loc ml_type locT_nat).
 
 Let cnew T (v : coq_type T) : M (loc T) :=
   fun st => let n := size st in
-            Ret (mkloc T n, rcons st (mkbind (v : coq_type T))).
+            Ret (mkloc T n, rcons st (mkbind v)).
 
 Let cget T (r : loc T) : M (coq_type T) :=
   fun st =>
@@ -1774,7 +1773,7 @@ Let cput T (r : loc T) (v : coq_type T) : M unit :=
     let n := loc_id r in
     if nth_error st n is Some (mkbind T' _) then
       if coerce T' v is Some u then
-        Ret (tt, set_nth def st n (mkbind (u : coq_type _)))
+        Ret (tt, set_nth def st n (mkbind u))
       else fail
     else fail.