From 64ce7859dc05816dbd383b580f3c9952faf230ed Mon Sep 17 00:00:00 2001 From: Yannick Forster Date: Tue, 17 Oct 2023 17:49:53 +0200 Subject: [PATCH] Replace elimtype False by exfalso (#995) --- .github/nix-action-coq-8.17-macos.yml | 199 ------------------- .github/nix-action-coq-8.17-ubuntu.yml | 199 ------------------- .github/workflows/build.yml | 3 +- coq-metacoq-common.opam | 2 +- coq-metacoq-erasure-plugin.opam | 2 +- coq-metacoq-erasure.opam | 2 +- coq-metacoq-pcuic.opam | 2 +- coq-metacoq-quotation.opam | 2 +- coq-metacoq-safechecker-plugin.opam | 2 +- coq-metacoq-safechecker.opam | 2 +- coq-metacoq-template-pcuic.opam | 2 +- coq-metacoq-template.opam | 2 +- coq-metacoq-translations.opam | 2 +- coq-metacoq-utils.opam | 6 +- coq-metacoq.opam | 2 +- erasure/theories/ErasureFunction.v | 4 +- erasure/theories/ErasureFunctionProperties.v | 18 +- 17 files changed, 26 insertions(+), 425 deletions(-) delete mode 100644 .github/nix-action-coq-8.17-macos.yml delete mode 100644 .github/nix-action-coq-8.17-ubuntu.yml diff --git a/.github/nix-action-coq-8.17-macos.yml b/.github/nix-action-coq-8.17-macos.yml deleted file mode 100644 index 001970309..000000000 --- a/.github/nix-action-coq-8.17-macos.yml +++ /dev/null @@ -1,199 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: macos-latest - concurrency: - group: ${{ github.workflow }}-MacOS-coq-${{ github.event_name }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - with: - 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 - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: metacoq - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-dev\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "coq" - equations: - needs: - - coq - runs-on: macos-latest - concurrency: - group: ${{ github.workflow }}-MacOS-equations-${{ github.event_name }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - with: - 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 - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: metacoq - - id: stepCheck - name: Checking presence of CI target equations - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-dev\" --argstr job \"equations\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "equations" - metacoq: - needs: - - coq - - equations - runs-on: macos-latest - concurrency: - group: ${{ github.workflow }}-MacOS-metacoq-${{ github.event_name }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - with: - 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 - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: metacoq - - id: stepCheck - name: Checking presence of CI target metacoq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-dev\" --argstr job \"metacoq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: equations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "equations" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-utils' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-utils" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-common' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-common" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-template-coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-template-coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-pcuic' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-pcuic" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-safechecker' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-safechecker" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-template-pcuic' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-template-pcuic" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-erasure' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-erasure" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-quotation' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-quotation" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-safechecker-plugin' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-safechecker-plugin" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-erasure-plugin' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-erasure-plugin" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq" -name: Nix CI for bundle coq-dev -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - main - - coq-dev diff --git a/.github/nix-action-coq-8.17-ubuntu.yml b/.github/nix-action-coq-8.17-ubuntu.yml deleted file mode 100644 index 3240631ec..000000000 --- a/.github/nix-action-coq-8.17-ubuntu.yml +++ /dev/null @@ -1,199 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - concurrency: - group: ${{ github.workflow }}-Ubuntu-coq-${{ github.event_name }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - with: - 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 - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: metacoq - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-dev\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "coq" - equations: - needs: - - coq - runs-on: ubuntu-latest - concurrency: - group: ${{ github.workflow }}-Ubuntu-equations-${{ github.event_name }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - with: - 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 - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: metacoq - - id: stepCheck - name: Checking presence of CI target equations - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-dev\" --argstr job \"equations\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "equations" - metacoq: - needs: - - coq - - equations - runs-on: ubuntu-latest - concurrency: - group: ${{ github.workflow }}-Ubuntu-metacoq-${{ github.event_name }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - steps: - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ - \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ - \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - with: - 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 - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: metacoq - - id: stepCheck - name: Checking presence of CI target metacoq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-dev\" --argstr job \"metacoq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: equations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "equations" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-utils' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-utils" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-common' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-common" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-template-coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-template-coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-pcuic' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-pcuic" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-safechecker' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-safechecker" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-template-pcuic' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-template-pcuic" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-erasure' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-erasure" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-quotation' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-quotation" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-safechecker-plugin' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-safechecker-plugin" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-erasure-plugin' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq-erasure-plugin" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-dev" - --argstr job "metacoq" -name: Nix CI for bundle coq-dev -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - main - - coq-dev diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index b6f3cf815..0077acc3b 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -24,7 +24,7 @@ jobs: strategy: matrix: coq_version: - - '8.18' + - 'dev' ocaml_version: - '4.14-flambda' target: [ local, opam, quick ] @@ -55,7 +55,6 @@ 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" diff --git a/coq-metacoq-common.opam b/coq-metacoq-common.opam index cd4ae3fc6..45a73ba75 100644 --- a/coq-metacoq-common.opam +++ b/coq-metacoq-common.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.18.dev" +version: "dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" diff --git a/coq-metacoq-erasure-plugin.opam b/coq-metacoq-erasure-plugin.opam index c480c7e98..884d6a877 100644 --- a/coq-metacoq-erasure-plugin.opam +++ b/coq-metacoq-erasure-plugin.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.18.dev" +version: "dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" diff --git a/coq-metacoq-erasure.opam b/coq-metacoq-erasure.opam index 0eecc5523..b2dd484f9 100644 --- a/coq-metacoq-erasure.opam +++ b/coq-metacoq-erasure.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.18.dev" +version: "dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" diff --git a/coq-metacoq-pcuic.opam b/coq-metacoq-pcuic.opam index 87791e67c..f8abf0db5 100644 --- a/coq-metacoq-pcuic.opam +++ b/coq-metacoq-pcuic.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.18.dev" +version: "dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" diff --git a/coq-metacoq-quotation.opam b/coq-metacoq-quotation.opam index d36813915..59f5f9d3b 100644 --- a/coq-metacoq-quotation.opam +++ b/coq-metacoq-quotation.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.18.dev" +version: "dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" diff --git a/coq-metacoq-safechecker-plugin.opam b/coq-metacoq-safechecker-plugin.opam index 10825a6a3..c691fdba0 100644 --- a/coq-metacoq-safechecker-plugin.opam +++ b/coq-metacoq-safechecker-plugin.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.18.dev" +version: "dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" diff --git a/coq-metacoq-safechecker.opam b/coq-metacoq-safechecker.opam index 4ec7b94bc..7594e7991 100644 --- a/coq-metacoq-safechecker.opam +++ b/coq-metacoq-safechecker.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.18.dev" +version: "dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" diff --git a/coq-metacoq-template-pcuic.opam b/coq-metacoq-template-pcuic.opam index 18aa8302c..1a0848d0c 100644 --- a/coq-metacoq-template-pcuic.opam +++ b/coq-metacoq-template-pcuic.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.18.dev" +version: "dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" diff --git a/coq-metacoq-template.opam b/coq-metacoq-template.opam index a6ac991a0..8d0ff8ed7 100644 --- a/coq-metacoq-template.opam +++ b/coq-metacoq-template.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.18.dev" +version: "dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" diff --git a/coq-metacoq-translations.opam b/coq-metacoq-translations.opam index 409ce2ee3..5db167651 100644 --- a/coq-metacoq-translations.opam +++ b/coq-metacoq-translations.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.18.dev" +version: "dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" diff --git a/coq-metacoq-utils.opam b/coq-metacoq-utils.opam index 3593a7aca..497c11b53 100644 --- a/coq-metacoq-utils.opam +++ b/coq-metacoq-utils.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.18.dev" +version: "dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" @@ -29,8 +29,8 @@ install: [ ] depends: [ "stdlib-shims" - "coq" { >= "8.18" & < "8.19~" } - "coq-equations" { = "1.3+8.18" } + "coq" { = "dev" } + "coq-equations" { = "dev" } ] synopsis: "The utility library of Template Coq and PCUIC" description: """ diff --git a/coq-metacoq.opam b/coq-metacoq.opam index 0995857c4..0e36fb32c 100644 --- a/coq-metacoq.opam +++ b/coq-metacoq.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "8.18.dev" +version: "dev" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" diff --git a/erasure/theories/ErasureFunction.v b/erasure/theories/ErasureFunction.v index 4cc87e860..be3895e5a 100644 --- a/erasure/theories/ErasureFunction.v +++ b/erasure/theories/ErasureFunction.v @@ -322,7 +322,7 @@ Proof. + intros hl. case: (knset_mem_spec kn0 _) => hin. - * elimtype False. + * exfalso. eapply lookup_global_deps in hl; tea. now eapply fresh_global_In in H1. * case: (knset_mem_spec kn0 _). @@ -641,7 +641,7 @@ Proof. * rewrite global_deps_union KernameSet.union_spec. intros [] fr. ** depelim fr. now eapply IHΣ. - ** depelim fr. elimtype False. eapply IHΣ in H1; eauto. + ** depelim fr. exfalso. eapply IHΣ in H1; eauto. destruct d as [[[]]|] eqn:eqd; cbn in H. + cbn in H1. eapply (term_global_deps_fresh Σ) in H1; tea. cbn in H2. eapply (Forall_map (fun x => x <> kn) fst) in fr. diff --git a/erasure/theories/ErasureFunctionProperties.v b/erasure/theories/ErasureFunctionProperties.v index fe2dd16db..9662d8a71 100644 --- a/erasure/theories/ErasureFunctionProperties.v +++ b/erasure/theories/ErasureFunctionProperties.v @@ -215,7 +215,7 @@ Proof. pose proof (wf' := wf.1). specialize (H1 kn). forward H1. now rewrite KernameSet.singleton_spec. red in H1. destruct H1. - elimtype False. destruct H1 as [cst [declc _]]. + exfalso. destruct H1 as [cst [declc _]]. { destruct x1 as [d _]. unshelve eapply declared_minductive_to_gen in d; eauto. unshelve eapply declared_constant_to_gen in declc; eauto. @@ -246,7 +246,7 @@ Proof. pose proof (wf' := wf.1). specialize (H0 (inductive_mind p.(proj_ind))). forward H0. now rewrite KernameSet.singleton_spec. red in H0. destruct H0. - elimtype False. destruct H0 as [cst [declc _]]. + exfalso. destruct H0 as [cst [declc _]]. { unshelve eapply declared_constant_to_gen in declc; eauto. red in declc. destruct d as [[[d _] _] _]. @@ -475,7 +475,7 @@ Lemma erase_global_includes X_type (X:X_type.π1) deps decls {normalization_in} includes_deps Σ (fst Σ') deps'. Proof. intros ? sub Σ wfΣ; cbn. induction decls in X, H, sub, prf, deps, deps', Σ , wfΣ, normalization_in |- *. - - simpl. intros i hin. elimtype False. + - simpl. intros i hin. exfalso. edestruct (H i hin) as [[decl Hdecl]]; eauto. rewrite /lookup_env (prf _ wfΣ) in Hdecl. noconf Hdecl. - intros i hin. @@ -950,7 +950,7 @@ Proof. ++ intros kn'deps kn'eg'. eapply in_erase_global_deps_acc in kn'eg'. destruct kn'eg'. eapply KernameSet.mem_spec in H. congruence. - elimtype False. clear -prf wfΣ H. + exfalso. clear -prf wfΣ H. specialize (prf _ wfΣ). pose proof (abstract_env_wf _ wfΣ) as []. eapply wf_fresh_globals in X0. rewrite prf in X0. depelim X0. @@ -965,7 +965,7 @@ Proof. ++ intros kn'deps kn'eg'. eapply in_erase_global_deps_acc in kn'eg'. destruct kn'eg'. eapply KernameSet.mem_spec in H. congruence. - elimtype False. clear -prf wfΣ H. + exfalso. clear -prf wfΣ H. specialize (prf _ wfΣ). pose proof (abstract_env_wf _ wfΣ) as []. eapply wf_fresh_globals in X0. rewrite prf in X0. depelim X0. @@ -1116,7 +1116,7 @@ Proof. now eapply in_global_deps. * intros hwf. case: (knset_mem_spec kn _); intros hin. - ** elimtype False. + ** exfalso. depelim hwf. eapply in_global_deps_fresh in hin => //. ** depelim hwf. rewrite -IHΣ => //. @@ -1132,7 +1132,7 @@ Proof. now eapply in_global_deps. ** intros hwf. case: (knset_mem_spec kn _); intros hin. - *** elimtype False. + *** exfalso. eapply in_global_deps_fresh in hin => //. *** rewrite -IHΣ => //. + intros wf; depelim wf. @@ -1150,7 +1150,7 @@ Proof. now eapply in_global_deps. ** intros hwf. case: (knset_mem_spec kn _); intros hin. - *** elimtype False. + *** exfalso. eapply in_global_deps_fresh in hin => //. *** rewrite -IHΣ => //. Qed. @@ -1978,7 +1978,7 @@ Proof. destruct (inspect_bool (is_erasableb X_type Xext [] t wt)) eqn:heq. - simp erase. rewrite heq. simp erase => //. - - elimtype False. + - exfalso. pose proof (abstract_env_exists X) as [[? wf]]. destruct (@is_erasableP X_type Xext _ [] t wt) => //. apply n. intros. sq. now rewrite (abstract_env_ext_irr _ H H2).