port to coq master

.github/workflows/main.yml

@@ -10,7 +10,7 @@ jobs:
         opam_file:
           - 'coq-autosubst-ocaml.opam'
         image:
-          - 'coqorg/coq:8.19-rc1-ocaml-4.14.1-flambda' 
+          - 'coqorg/coq:dev-ocaml-4.14.1-flambda'
       fail-fast: false  # don't stop jobs if one fails
     steps:
       - uses: actions/checkout@v2

README.md

@@ -114,9 +114,9 @@ First, install opam following the [directions for your operating system](https:/
 It is best practice to create a new opam switch to not cause conflicts with any of your other installed packages.
 We will also need to add the Coq repository and then we can install the `coq-autosubst-ocaml` package.
 ```bash
-$ opam switch create autosubst-ocaml ocaml-base-compiler.4.11.1
+$ opam switch create autosubst-master --packages="ocaml-variants.4.14.1+options,ocaml-option-flambda"
 $ eval $(opam env)
-$ opam repo add coq-released https://coq.inria.fr/opam/released
+$ opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
 $ opam install coq-autosubst-ocaml
 ```
 

coq-autosubst-ocaml.opam

@@ -11,12 +11,12 @@ description: """
 homepage: "https://github.com/uds-psl/autosubst-ocaml"
 bug-reports: "https://github.com/uds-psl/autosubst-ocaml/issues"
 maintainer: "Yannick Forster yannick.forster@inria.fr"
-authors: [ "Adrian Dapprich s8addapp@stud.uni-saarland.de" ]
+authors: [ "Adrian Dapprich" ]
 license: "MIT"
 
 depends: [
   "ocaml" { >= "4.09" & < "4.15" }
-  "coq" { >= "8.19" & < "8.20" }
+  "coq" { = "dev" }
   "angstrom" { >= "0.15.0" }
   "dune" { >= "2.5" }
   "ocamlgraph" { >= "2.0.0" }

lib/gallinaGen.ml

@@ -92,7 +92,7 @@ let binder_ ?(implicit=false) ?btype bnames =
   let open Constrexpr in
   let bk = Default (if implicit then Glob_term.MaxImplicit else Glob_term.Explicit) in
   let btype = Option.default (CAst.make @@ CHole None) btype in
-  CLocalAssum (List.map lname_ bnames, bk, btype)
+  CLocalAssum (List.map lname_ bnames, None, bk, btype)
 
 let binder1_ ?implicit ?btype bname =
   binder_ ?implicit ?btype [bname]
@@ -155,4 +155,4 @@ let setup_coq () =
       ; CAst.make (Vernacexpr.SetOnlyPrinting)
       ; CAst.make (Vernacexpr.SetAssoc Gramlib.Gramext.RightA) ]
     }) in
-  ()
+  ()