examples: Adapt to Coq 8.10

broSysX64 · Jan 15, 2020 · 2365f88 · 2365f88
1 parent b75fc77
commit 2365f88
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/examples/IO.v b/examples/IO.v
@@ -16,11 +16,11 @@ Definition example : itree IO unit :=
 Definition SOME_NUMBER := 13.
 
 Definition test_interp : itree IO unit -> bool := fun t =>
-  match t.(observe) with
+  match observe t with
   | VisF e k =>
     match e in IO X return (X -> _) -> _ with
     | Read => fun id =>
-      match (k (id SOME_NUMBER)).(observe) with
+      match observe (k (id SOME_NUMBER)) with
       | VisF (Write n) _ => n =? SOME_NUMBER
       | _ => false
       end

diff --git a/examples/Nimp.v b/examples/Nimp.v
@@ -16,7 +16,7 @@ Inductive com : Type :=
 | seq : com -> com -> com
 .
 
-Infix ";;" := seq (at level 60, right associativity) : com_scope.
+Infix ";;" := seq (at level 61, right associativity) : com_scope.
 Delimit Scope com_scope with com.
 Open Scope com_scope.