Fix compilation for ExtLib 1.2.1

liyishuai · Jan 28, 2024 · 693f36a · 693f36a
1 parent 2d1d11e
commit 693f36a
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 2 deletions.
diff --git a/Decode.v b/Decode.v
@@ -52,7 +52,7 @@ Instance JDecode__bool : JDecode bool :=
 
 Definition decode__list {T} `{JDecode T} : JDecode (list T) :=
   fun j : json =>
-    if j is JSON__Array l then sequence $ map decode l
+    if j is JSON__Array l then @sequence list _ _ _ _ $ map decode l
     else inl $ "Not an Array: " ++ to_string j.
 
 Definition decode__option {T} `{JDecode T} : JDecode (option T) :=

diff --git a/JSON.v b/JSON.v
@@ -3,6 +3,7 @@ From ExtLib Require Export
      List
      Traversable
      Monad
+     Option
      OptionMonad.
 From Coq Require Export
      Basics
@@ -59,7 +60,7 @@ Definition get_bool (k : string) (j : json) : option bool :=
 
 Definition get_list {T} (f : json -> option T) (j : json) : option (list T) :=
   if j is JSON__Array l
-  then sequence (map f l)
+  then @sequence _ _ option _ _ (map f l)
   else None.
 
 Definition get_nth (n : nat) (j : json) : option json :=

diff --git a/coq-json.opam b/coq-json.opam
@@ -19,6 +19,7 @@ run-test: [make "-j%{jobs}%" "test"]
 install: [make "install"]
 depends: [
   "coq" { >= "8.14~" }
+  "coq-ext-lib"
   "coq-parsec" { >= "0.1.1" }
   "menhir" { >= "20220210" }
   "coq-menhirlib" { >= "20220210" }