Merge 8.16, 8.17 and 8.18 into main

.github/dependabot.yml

@@ -9,3 +9,27 @@ updates:
       interval: "daily"
     labels:
       - "dependencies"
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    target-branch: "main"
+    schedule:
+      # Check for updates to GitHub Actions every weekday
+      interval: "daily"
+    labels:
+      - "dependencies"
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    target-branch: "coq-8.17"
+    schedule:
+      # Check for updates to GitHub Actions every weekday
+      interval: "daily"
+    labels:
+      - "dependencies"
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    target-branch: "coq-8.16"
+    schedule:
+      # Check for updates to GitHub Actions every weekday
+      interval: "daily"
+    labels:
+      - "dependencies"

.github/workflows/nix-action-coq-dev-macos.yml → .github/nix-action-coq-8.17-macos.yml

@@ -19,7 +19,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
+<<<<<<<< HEAD:.github/workflows/nix-action-coq-dev-macos.yml
       uses: cachix/install-nix-action@v22
+========
+      uses: cachix/install-nix-action@v23
+>>>>>>>> coq-8.17-updates-8.16:.github/nix-action-coq-8.17-macos.yml
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup metacoq
@@ -59,7 +63,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
+<<<<<<<< HEAD:.github/workflows/nix-action-coq-dev-macos.yml
       uses: cachix/install-nix-action@v22
+========
+      uses: cachix/install-nix-action@v23
+>>>>>>>> coq-8.17-updates-8.16:.github/nix-action-coq-8.17-macos.yml
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup metacoq
@@ -104,7 +112,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
+<<<<<<<< HEAD:.github/workflows/nix-action-coq-dev-macos.yml
       uses: cachix/install-nix-action@v22
+========
+      uses: cachix/install-nix-action@v23
+>>>>>>>> coq-8.17-updates-8.16:.github/nix-action-coq-8.17-macos.yml
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup metacoq

.github/workflows/nix-action-coq-dev-ubuntu.yml → .github/nix-action-coq-8.17-ubuntu.yml

@@ -19,7 +19,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
+<<<<<<<< HEAD:.github/workflows/nix-action-coq-dev-ubuntu.yml
       uses: cachix/install-nix-action@v22
+========
+      uses: cachix/install-nix-action@v23
+>>>>>>>> coq-8.17-updates-8.16:.github/nix-action-coq-8.17-ubuntu.yml
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup metacoq
@@ -59,7 +63,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
+<<<<<<<< HEAD:.github/workflows/nix-action-coq-dev-ubuntu.yml
       uses: cachix/install-nix-action@v22
+========
+      uses: cachix/install-nix-action@v23
+>>>>>>>> coq-8.17-updates-8.16:.github/nix-action-coq-8.17-ubuntu.yml
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup metacoq
@@ -104,7 +112,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
+<<<<<<<< HEAD:.github/workflows/nix-action-coq-dev-ubuntu.yml
       uses: cachix/install-nix-action@v22
+========
+      uses: cachix/install-nix-action@v23
+>>>>>>>> coq-8.17-updates-8.16:.github/nix-action-coq-8.17-ubuntu.yml
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup metacoq

.github/workflows/build.yml

@@ -24,7 +24,7 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - 'dev'
+          - '8.18'
         ocaml_version:
           - '4.14-flambda'
         target: [ local, opam, quick ]
@@ -55,6 +55,7 @@ jobs:
             startGroup "Print opam config"
               sudo chown -R coq:coq .
               opam config list; opam repo list; opam list
+              opam pin -y coq-equations.1.3+8.18 "https://github.com/mattam82/Coq-Equations.git#8.18"
             endGroup
           script: |
             startGroup "Build project"

.gitignore

@@ -405,3 +405,5 @@ erasure-plugin/Makefile.erasureplugin
 erasure-plugin/Makefile.erasureplugin.conf
 erasure-plugin/Makefile.plugin
 erasure-plugin/Makefile.plugin.conf
+erasure-plugin/META
+safechecker-plugin/META

.vscode/metacoq.code-workspace

@@ -10,6 +10,7 @@
         "coqtop.args": [
 
 
+
 			"-R", "safechecker-plugin/theories", "MetaCoq.SafeCheckerPlugin",
 
 			"-R", "utils/theories", "MetaCoq.Utils",
@@ -27,6 +28,7 @@
 		"-R", "safechecker/theories", "MetaCoq.SafeChecker",
 		"-I", "erasure/src",
 		"-R", "erasure/theories", "MetaCoq.Erasure",
+		"-R", "erasure-plugin/theories", "MetaCoq.ErasurePlugin",
 		"-R", "translations", "MetaCoq.Translations",
 		"-R", "test-suite/plugin-demo/theories", "MetaCoq.ExtractedPluginDemo",
 		"-R", "test-suite", "MetaCoq.TestSuite"

DOC.md

@@ -2,8 +2,7 @@
 
 ## Branches and compatibility
 
-**tl;dr** You should do your PRs against [coq-8.16](https://github.com/MetaCoq/metacoq/tree/coq-8.16).
-
+**tl;dr** You should do your PRs against [coq-8.18](https://github.com/MetaCoq/metacoq/tree/coq-8.16).
 
 Coq's kernel API is not stable yet, and changes there are reflected in MetaCoq's reified structures,
 so we do not ensure any compatibility from version to version. There is one branch for each Coq version.
@@ -22,8 +21,8 @@ stable release of Coq.
 <!-- gets backports from `coq-8.11` when possible. Both `coq-8.11` and `coq-8.10` have associated -->
 <!-- "alpha"-quality `opam` packages. -->
 
-The branches [coq-8.16](https://github.com/MetaCoq/metacoq/tree/coq-8.16) and [coq-8.17](https://github.com/MetaCoq/metacoq/tree/coq-8.17) are being kept in sync.
-The branches [coq-8.6](https://github.com/MetaCoq/metacoq/tree/coq-8.6) to [coq-8.15](https://github.com/MetaCoq/metacoq/tree/coq-8.15) are frozen.
+The branches [coq-8.17](https://github.com/MetaCoq/metacoq/tree/coq-8.17) and [coq-8.18](https://github.com/MetaCoq/metacoq/tree/coq-8.18) are being kept in sync.
+The branches [coq-8.6](https://github.com/MetaCoq/metacoq/tree/coq-8.6) to [coq-8.15](https://github.com/MetaCoq/metacoq/tree/coq-8.16) are frozen.
 
 
 ## Program and Equations

INSTALL.md

@@ -55,8 +55,7 @@ To compile the library, you need:
 
 - The `Coq` version corrsponding to your branch (you can use the `coq.dev` package
   for the `main` branch).
-- `OCaml` (tested with `4.06.1`, `4.07.1`, and `4.10.0`, beware that `OCaml 4.06.0`
-  can produce linking errors on some platforms)
+- `OCaml` (tested with `4.14.0`)
 - [`Equations 1.3`](http://mattam82.github.io/Coq-Equations/)
 
 The recommended way to build a development environment for MetaCoq is
@@ -67,10 +66,10 @@ to have a dedicated `opam` switch (see below).
 To get the source code:
 
     # git clone https://github.com/MetaCoq/metacoq.git
-    # git checkout -b coq-8.17 origin/coq-8.17
+    # git checkout -b coq-8.18 origin/coq-8.18
     # git status
 
-This checks that you are indeed on the `coq-8.17` branch.
+This checks that you are indeed on the `coq-8.18` branch.
 
 ### Setting up an `opam` switch
 
@@ -79,10 +78,10 @@ To setup a fresh `opam` installation, you might want to create a
 one yet. You need to use **opam 2** to obtain the right version of
 `Equations`.
 
-    # opam switch create coq.8.17 --packages=ocaml-variants.4.13.1+options,ocaml-option-flambda
+    # opam switch create coq.8.18 --packages="ocaml-variants.4.14.0+options,ocaml-option-flambda"
     # eval $(opam env)
 
-This creates the `coq.8.17` switch which initially contains only the
+This creates the `coq.8.18` switch which initially contains only the
 basic `OCaml` `4.13.1` compiler with the `flambda` option enabled,
 and puts you in the right environment (check with `ocamlc -v`).
 
@@ -96,7 +95,7 @@ If the commands are successful you should have `coq` available (check with `coqc
 **Remark:** You can create a [local switch](https://opam.ocaml.org/blog/opam-20-tips/#Local-switches) for
 developing using (in the root directory of the sources):
 
-    # opam switch create . 4.07.1
+    # opam switch create . --packages="ocaml-variants.4.14.0+options,ocaml-option-flambda"
 
 Or use `opam switch link foo` to link an existing opam switch `foo` with
 the sources directory.

Makefile

@@ -1,5 +1,5 @@
 
-all: printconf template-coq pcuic safechecker erasure examples test-suite translations quotation
+all: printconf template-coq pcuic safechecker erasure erasure-plugin 
 
 -include Makefile.conf
 
@@ -26,7 +26,7 @@ else
 endif
 endif
 
-install: all translations
+install: all 
 	$(MAKE) -C utils install
 	$(MAKE) -C common install
 	$(MAKE) -C template-coq install
@@ -36,7 +36,7 @@ install: all translations
 	$(MAKE) -C quotation install
 	$(MAKE) -C safechecker-plugin install
 	$(MAKE) -C erasure install
-	$(MAKE) -C translations install
+	$(MAKE) -C erasure-plugin install
 
 uninstall:
 	$(MAKE) -C utils uninstall
@@ -48,6 +48,7 @@ uninstall:
 	$(MAKE) -C quotation uninstall
 	$(MAKE) -C safechecker-plugin uninstall
 	$(MAKE) -C erasure uninstall
+	$(MAKE) -C erasure-plugin uninstall
 	$(MAKE) -C translations uninstall
 
 html: all
@@ -175,7 +176,7 @@ cleanplugins:
 
 ci-local-noclean:
 	./configure.sh local
-	$(MAKE) all test-suite TIMED=pretty-timed
+	$(MAKE) all translations test-suite TIMED=pretty-timed
 
 ci-local: ci-local-noclean
 	$(MAKE) clean

common/_CoqProject.in

@@ -11,5 +11,6 @@ theories/MonadBasicAst.v
 theories/Environment.v
 theories/Reflect.v
 theories/EnvironmentTyping.v
+theories/EnvironmentReflect.v
 theories/EnvMap.v
 theories/Transform.v