Fix compilation for ExtLib 1.2.1

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) :=

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 :=

Makefile

@@ -21,4 +21,4 @@ test:
 
 publish%:
 	opam publish --packages-directory=released/packages \
-		--repo=coq/opam-coq-archive --tag=v$* -v $* liyishuai/coq-json
+		--repo=coq/opam --tag=v$* -v $* liyishuai/coq-json

README.md

@@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/liyishuai/coq-json/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/liyishuai/coq-json/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/liyishuai/coq-json/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/liyishuai/coq-json/actions/workflows/docker-action.yml
 
 
 
@@ -22,6 +22,7 @@ From JSON to Coq, and vice versa.
 - Compatible Coq versions: 8.14 or later
 - Additional dependencies:
   - [Parsec](https://github.com/liyishuai/coq-parsec)
+  - [ExtLib](https://coq-community.org/coq-ext-lib)
   - [Menhir](http://gallium.inria.fr/~fpottier/menhir/)
   - [MenhirLib](https://gitlab.inria.fr/fpottier/menhir/-/tree/master/coq-menhirlib/)
 - Coq namespace: `JSON`

coq-json.opam

@@ -20,6 +20,7 @@ install: [make "install"]
 depends: [
   "coq" { >= "8.14~" }
   "coq-parsec" { >= "0.1.1" }
+  "coq-ext-lib" 
   "menhir" { >= "20220210" }
   "coq-menhirlib" { >= "20220210" }
 ]
@@ -28,7 +29,6 @@ tags: [
   "category:Computer Science/Data Types and Data Structures"
   "keyword:serialization"
   "keyword:JSON"
-  "date:2022-05-31"
   "logpath:JSON"
 ]
 authors: [

meta.yml

@@ -18,6 +18,9 @@ dependencies:
     opam:
       name: coq-parsec
       version: '{ >= "0.1.1" }'
+  - description: '[ExtLib](https://coq-community.org/coq-ext-lib)'
+    opam:
+      name: coq-ext-lib
   - description: '[Menhir](http://gallium.inria.fr/~fpottier/menhir/)'
     opam:
       name: menhir
@@ -32,7 +35,6 @@ categories:
 keywords:
   - name: serialization
   - name: JSON
-date: 2022-05-31
 namespace: JSON
 opam-file-maintainer: 'Yishuai Li <[email protected]>'
 supported_coq_versions: