prepare for 8.20 release

Author: mrhaandi

.github/workflows/build.yml

@@ -12,7 +12,7 @@ jobs:
     strategy:
       matrix:
         coq_version: 
-          - 'dev'
+          - '8.20'
         ocaml_version:
           - '4.14-flambda'
       fail-fast: true

README.md

@@ -1,18 +1,3 @@
-# Manual installation for Coq
-
-```
-opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda
-eval $(opam env)
-opam pin add -k git coq-core.dev "https://github.com/coq/coq.git#master"
-opam pin add -k git coq-stdlib.dev "https://github.com/coq/coq.git#master"
-opam pin add -k git coqide-server.dev "https://github.com/coq/coq.git#master"
-opam pin add -k git coq.dev "https://github.com/coq/coq.git#master"
-opam pin add -k git coq-equations.dev "https://github.com/mattam82/Coq-Equations.git#main"
-opam pin add -k git coq-metacoq-utils.dev "https://github.com/MetaCoq/metacoq.git#main"
-opam pin add -k git coq-metacoq-common.dev "https://github.com/MetaCoq/metacoq.git#main"
-opam pin add -k git coq-metacoq-template.dev "https://github.com/MetaCoq/metacoq.git#main"
-```
-
 # Coq Library of Undecidability Proofs
 
 [![CI](https://github.com/uds-psl/coq-library-undecidability/workflows/CI/badge.svg?branch=master)](https://github.com/uds-psl/coq-library-undecidability/actions)
@@ -117,19 +102,37 @@ An equivalence proof that most of the mentioned models of computation compute th
 
 ## Manual Installation Instructions
 
-You need the `master` branch of `Coq` built on OCAML `>= 4.09.1`, and the Template-Coq (part of [MetaCoq](https://metacoq.github.io/)) package for Coq. If you are using opam 2 you can use the following commands to install the dependencies on a new switch:
+If you can use `opam 2` on your system, you can follow the instructions here.
+
+### Install from git via opam
+
+You can use `opam` to install the current state of this branch as follows.
+
+We recommend creating a fresh opam switch:
+
+```
+opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda
+eval $(opam env)
+```
+
+Then the following commands install the library:
+
+```
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam update
+opam pin add coq-library-undecidability.dev+8.20 "https://github.com/uds-psl/coq-library-undecidability.git#coq-8.20"
+```
+
+### Manual installation
+
+You need `Coq 8.20` built on OCAML `>= 4.09.1` (but we recommend and test OCaml version `4.14.1+flambda`) and the Template-Coq part of the [MetaCoq](https://metacoq.github.io/) package for Coq. If you are using `opam 2` you can use the following commands to install the dependencies on a new switch:
 
 ```
 opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda
 eval $(opam env)
-opam pin add -k git coq-core.dev "https://github.com/coq/coq.git#master"
-opam pin add -k git coq-stdlib.dev "https://github.com/coq/coq.git#master"
-opam pin add -k git coqide-server.dev "https://github.com/coq/coq.git#master"
-opam pin add -k git coq.dev "https://github.com/coq/coq.git#master"
-opam pin add -k git coq-equations.dev "https://github.com/mattam82/Coq-Equations.git#main"
-opam pin add -k git coq-metacoq-utils.dev "https://github.com/MetaCoq/metacoq.git#main"
-opam pin add -k git coq-metacoq-common.dev "https://github.com/MetaCoq/metacoq.git#main"
-opam pin add -k git coq-metacoq-template.dev "https://github.com/MetaCoq/metacoq.git#main"
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam update
+opam install . --deps-only
 ```
 
 #### Building the undecidability library
@@ -150,7 +153,7 @@ The library is compatible with Coq's compiled interfaces ([`vos`](https://coq.in
 
 #### Coq version
 
-Be careful that this branch only compiles under `Coq 8.16`. If you want to use a different Coq version you have to change to a different branch.
+Be careful that this branch only compiles under `Coq 8.20`. If you want to use a different Coq version you have to change to a different branch.
 Due to compatibility issues, not every branch contains exactly the same problems. 
 We recommend to use the newest branch if possible.
 

opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev+8.16"
+version: "dev+8.20"
 maintainer: "[email protected]"
 homepage: "https://github.com/uds-psl/coq-library-undecidability/"
 dev-repo: "git+https://github.com/uds-psl/coq-library-undecidability/"
@@ -26,12 +26,12 @@ install: [
   [make "install"]
 ]
 depends: [
-  "coq" {= "dev"}
+  "coq" {>= "8.20" & < "8.21~"}
   "ocaml"
-  "coq-metacoq-template" {= "dev"}
+  "coq-metacoq-template"
 ]
 
 synopsis: "A Coq Library of Undecidability Proofs"
 url {
-  git: "https://github.com/uds-psl/coq-library-undecidability.git#coq-8.16"
+  git: "https://github.com/uds-psl/coq-library-undecidability.git#coq-8.20"
 }

theories/FOL/Arithmetics/Signature.v

@@ -6,6 +6,8 @@ From Undecidability.Synthetic Require Import EnumerabilityFacts ListEnumerabilit
 Import Vector.VectorNotations.
 Require Import List.
 
+Unset Automatic Proposition Inductives.
+
 (* ** Signature for PA axiomatisation, containing function symbols for set operations *)
 
 #[global]

theories/FOL/Semantics/FiniteTarski/DoubleNegation.v

@@ -8,6 +8,8 @@ From Coq Require Import Arith Lia List.
 From Undecidability.Shared.Libs.DLW.Wf Require Import wf_finite.
 From Undecidability.Synthetic Require Import Definitions.
 
+Unset Automatic Proposition Inductives.
+
 Set Default Goal Selector "!".
 Set Mangle Names.
 Inductive syms_func : Type := .

theories/FOL/Syntax/Core.v

@@ -8,7 +8,7 @@ Import ListAutomationNotations.
 Import Coq.Vectors.Vector.
 Local Notation vec := t.
 
-
+Unset Automatic Proposition Inductives.
 
 Inductive peirce := class | intu.
 Existing Class peirce.

theories/SOL/PA2.v

@@ -4,6 +4,7 @@ Require Import Undecidability.SOL.SOL.
 Require Import Vector.
 Import VectorNotations SOLNotations.
 
+Unset Automatic Proposition Inductives.
 
 (* ** Signature of PA2 *)
 

theories/Shared/Libs/DLW/Utils/sorting.v

@@ -387,7 +387,7 @@ End sum_bounded_permutation.
 
 Section sum_bijection.
 
-  Inductive bijection n g h : Type :=
+  Inductive bijection n g h : Prop :=
     | in_bij : (forall i, i < n -> g i < n)
             -> (forall i, i < n -> h i < n) 
             -> (forall i, i < n -> g (h i) = i)

theories/_CoqProject

@@ -1,6 +1,6 @@
 -Q . Undecidability
 
--arg -w -arg -notation-overridden,-stdlib-vector,-notation-incompatible-prefix
+-arg -w -arg -notation-overridden,-stdlib-vector,-notation-incompatible-prefix,-postfix-notation-not-level-1,-closed-notation-not-level-0
 -arg "-set" -arg "'Default Proof Using = Type'"
 COQDOCFLAGS = "--charset utf-8 -s --with-header ../website/resources/header.html --with-footer ../website/resources/footer.html --index indexpage"