drop 8.19

.github/workflows/doc.yml

@@ -25,7 +25,7 @@ jobs:
     - name: setup ocaml
       uses: avsm/setup-ocaml@v1
       with:
-        ocaml-version: 4.10.1
+        ocaml-version: 4.14.2
 
     - name: install deps
       run: |
@@ -34,7 +34,7 @@ jobs:
         opam repo add coq-dev https://coq.inria.fr/opam/core-dev
         opam repo add extra-dev https://coq.inria.fr/opam/extra-dev
         opam update
-        opam install coq-serapi ./coq-elpi.opam coq-core.8.19.1
+        opam install coq-serapi.8.20.0+0.20.0 ./coq-elpi.opam coq-core.8.20.0
         sudo apt-get update
         sudo apt-get install python3-pip -y
         pip3 install git+https://github.com/cpitclaudel/alectryon.git@c8ab1ec

.github/workflows/main.yml

@@ -31,15 +31,17 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq_version: [ '8.19.2' , '8.20+rc1' , 'dev' ]
+        coq_version: [ '8.20+rc1' , 'dev' ]
         ocaml_version:
           - '4.14.x'
           - '5.2.x'
     steps:
     - uses: actions/checkout@v2
-    - uses: avsm/setup-ocaml@v2
+    - uses: avsm/setup-ocaml@v3
       with:
         ocaml-compiler: ${{ matrix.ocaml_version }}
+        opam-pin: false
+        opam-local-packages:
     - run: opam repo add coq-dev https://coq.inria.fr/opam/core-dev
     - run: opam install coq-core.${{ matrix.coq_version }}
     - run: opam install coq-stdlib.${{ matrix.coq_version }}

.nix/config.nix

@@ -27,15 +27,6 @@ let master = [
   default-bundle = "coq-8.20";
   bundles = {
 
-    "coq-8.19" = {
-      coqPackages = common-bundles // {
-        coq.override.version = "8.19";
-      };
-      ocamlPackages = {
-        elpi.override.version = "v1.19.5";
-      };
-    };
-
     "coq-8.20" = {
       coqPackages = common-bundles // {
         coq.override.version = "8.20";

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"a9f1e055901cba59260d03d64f523089bf63169c"
+"24e96b4870378d5e87fd2d0dd46405b471c286ab"

apps/coercion/src/coq_elpi_coercion_hook.mlg

@@ -7,14 +7,6 @@ open Elpi_plugin
 open Coq_elpi_arg_syntax
 open Coq_elpi_vernacular
 
-[%%if coq = "8.19" ]
-let relevant = Sorts.Relevant
-let anonR = Context.anonR
-let nameR = Context.nameR
-let annotR = Context.annotR
-let build_expected_type env sigma expected = sigma, expected, false
-let return s g _ = Some (s,g)
-[%%else]
 let relevant = EConstr.ERelevance.relevant
 let anonR = Context.make_annot Names.Name.Anonymous EConstr.ERelevance.irrelevant 
 let nameR x = Context.make_annot (Names.Name.Name x) EConstr.ERelevance.irrelevant 
@@ -30,7 +22,6 @@ let build_expected_type env sigma expected =
     sigma, EConstr.mkProd (annotR (Names.Name (Namegen.default_type_ident)), source, target), true
   | Coercion.Sort -> let (sigma, t) = Evarutil.new_Type sigma in sigma, t, true
 let return s g t = Some (s,g,t)
-[%%endif]
 
 let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
   let loc = API.Ast.Loc.initial "(unknown)" in