hide dirty type parameters

affeldt-aist · Jul 27, 2023 · cd60d9d · cd60d9d
1 parent 3e0e81d
commit cd60d9d
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/example_typed_store.v b/example_typed_store.v
@@ -561,6 +561,8 @@ Definition empty_env := @typed_store_model.mkEnv ml_type nil.
 Definition it0 : W unit := inr (tt, empty_env).
 
 Local Open Scope do_notation.
+Local Notation mkloc := (mkloc (locT:=monad_model.locT_nat)).
+Local Notation coq_type := (coq_type _).
 
 Definition incr (l : loc ml_int) : M int :=
   do x <- cget l; do _ <- cput l (Uint63.succ x); Ret (Uint63.succ x).