Replace 8.12 in all files with 8.13

DOC.md

@@ -13,19 +13,19 @@ The *main branch* or *current branch* is the one which appers when you go on
 Currently (unless you are reading the README of an outdated branch),
 it is the [coq-8.11](https://github.com/MetaCoq/metacoq/tree/coq-8.11).
 You should use it both for usage of MetaCoq and development of MetaCoq.
-We should move soon to [coq-8.12](https://github.com/MetaCoq/metacoq/tree/coq-8.12).
+We should move soon to [coq-8.13](https://github.com/MetaCoq/metacoq/tree/coq-8.12).
 
 The [master](https://github.com/MetaCoq/metacoq/tree/master) branch is following Coq's master
 branch and gets regular updates from the the main development branch which follows the latest
 stable release of Coq.
 
-The branch [coq-8.10](https://github.com/MetaCoq/metacoq/tree/coq-8.10)
-gets backports from `coq-8.11` when possible. Both `coq-8.11` and `coq-8.10` have associated
-"alpha"-quality `opam` packages.
+<!-- The branch ... -->
+<!-- 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.6](https://github.com/MetaCoq/metacoq/tree/coq-8.6),
 [coq-8.7](https://github.com/MetaCoq/metacoq/tree/coq-8.7), [coq-8.8](https://github.com/MetaCoq/metacoq/tree/coq-8.8)
-and [coq-8.9](https://github.com/MetaCoq/metacoq/tree/coq-8.9) are frozen.
+and [coq-8.9](https://github.com/MetaCoq/metacoq/tree/coq-8.9), and [coq-8.10](https://github.com/MetaCoq/metacoq/tree/coq-8.10) are frozen.
 
 
 

INSTALL.md

@@ -61,10 +61,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.12 origin/coq-8.12
+    # git checkout -b coq-8.13 origin/coq-8.13
     # git status
 
-This checks that you are indeed on the `coq-8.12` branch.
+This checks that you are indeed on the `coq-8.13` branch.
 
 ### Setting up an `opam` switch
 
@@ -73,10 +73,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.12 4.07.1
+    # opam switch create coq.8.13 4.07.1
     # eval $(opam env)
 
-This creates the `coq.8.12` switch which initially contains only the
+This creates the `coq.8.13` switch which initially contains only the
 basic `OCaml` `4.07.1` compiler, and puts you in the right environment
 (check with `ocamlc -v`).
 

README.md

@@ -4,7 +4,7 @@
 <img src="https://raw.githubusercontent.com/MetaCoq/metacoq.github.io/master/assets/LOGO.png" alt="MetaCoq" width="50px"/>
 </p>
 
-[![Build status](https://github.com/MetaCoq/metacoq/workflows/Test%20compilation/badge.svg?branch=coq-8.12)](https://github.com/MetaCoq/metacoq/actions) [![MetaCoq Chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com)
+[![Build status](https://github.com/MetaCoq/metacoq/workflows/Test%20compilation/badge.svg?branch=coq-8.13)](https://github.com/MetaCoq/metacoq/actions) [![MetaCoq Chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com)
 
 MetaCoq is a project formalizing Coq in Coq and providing tools for
 manipulating Coq terms and developing certified plugins
@@ -24,7 +24,7 @@ manipulating Coq terms and developing certified plugins
 
 ## Getting started
 
-- You may want to start with a [demo](https://github.com/MetaCoq/metacoq/tree/coq-8.12/examples/demo.v).
+- You may want to start with a [demo](https://github.com/MetaCoq/metacoq/tree/coq-8.13/examples/demo.v).
 
 - The current branch [documentation (as light coqdoc files)](https://metacoq.github.io/html/toc.html).
 
@@ -34,13 +34,13 @@ manipulating Coq terms and developing certified plugins
 
 ## Installation instructions
 
-See [INSTALL.md](https://github.com/MetaCoq/metacoq/tree/coq-8.12/INSTALL.md)
+See [INSTALL.md](https://github.com/MetaCoq/metacoq/tree/coq-8.13/INSTALL.md)
 
 
 
 ## Documentation
 
-See [DOC.md](https://github.com/MetaCoq/metacoq/tree/coq-8.12/DOC.md)
+See [DOC.md](https://github.com/MetaCoq/metacoq/tree/coq-8.13/DOC.md)
 
 
 
@@ -50,7 +50,7 @@ At the center of this project is the Template-Coq quoting library for
 Coq. The project currently has a single repository extending
 Template-Coq with additional features. Each extension is in dedicated folder.
 
-### [Template-Coq](https://github.com/MetaCoq/metacoq/tree/coq-8.12/template-coq)
+### [Template-Coq](https://github.com/MetaCoq/metacoq/tree/coq-8.13/template-coq)
 
 Template-Coq is a quoting library for [Coq](http://coq.inria.fr). It
 takes `Coq` terms and constructs a representation of their syntax tree as
@@ -92,7 +92,7 @@ calculus has proofs of standard metatheoretical results:
   that singleton elimination (from Prop to Type) is only allowed
   on singleton inductives in Prop.
 
-### [Safe Checker](https://github.com/MetaCoq/metacoq/tree/coq-8.12/safechecker)
+### [Safe Checker](https://github.com/MetaCoq/metacoq/tree/coq-8.13/safechecker)
 
 Implementation of a fuel-free and verified reduction machine, conversion
 checker and type checker for PCUIC. This relies on a postulate of
@@ -109,7 +109,7 @@ type-checker, one can use:
     MetaCoq CoqCheck <term>
 
 
-### [Erasure](https://github.com/MetaCoq/metacoq/tree/coq-8.12/erasure)
+### [Erasure](https://github.com/MetaCoq/metacoq/tree/coq-8.13/erasure)
 
 An erasure procedure to untyped lambda-calculus accomplishing the
 same as the Extraction plugin of Coq. The extracted safe erasure is
@@ -120,22 +120,22 @@ available in Coq through a new vernacular command:
 After importing `MetaCoq.Erasure.Loader`.
 
 
-### [Translations](https://github.com/MetaCoq/metacoq/tree/coq-8.12/translations)
+### [Translations](https://github.com/MetaCoq/metacoq/tree/coq-8.13/translations)
 
 Examples of translations built on top of this:
 
-- a parametricity plugin in [translations/param_original.v](https://github.com/MetaCoq/metacoq/tree/coq-8.12/translations/param_original.v)
+- a parametricity plugin in [translations/param_original.v](https://github.com/MetaCoq/metacoq/tree/coq-8.13/translations/param_original.v)
 
-- a plugin to negate funext in [translations/times_bool_fun.v](https://github.com/MetaCoq/metacoq/tree/coq-8.12/translations/times_bool_fun.v)
+- a plugin to negate funext in [translations/times_bool_fun.v](https://github.com/MetaCoq/metacoq/tree/coq-8.13/translations/times_bool_fun.v)
 
 
 ### Examples
 
 - An example Coq plugin built on the Template Monad, which can be used to
-  add a constructor to any inductive type is in [examples/add_constructor.v](https://github.com/MetaCoq/metacoq/tree/coq-8.12/examples/add_constructor.v)
+  add a constructor to any inductive type is in [examples/add_constructor.v](https://github.com/MetaCoq/metacoq/tree/coq-8.13/examples/add_constructor.v)
 
-- The test-suite files [test-suite/erasure_test.v](https://github.com/MetaCoq/metacoq/tree/coq-8.12/test-suite/erasure_test.v)
-  and [test-suite/safechecker_test.v](https://github.com/MetaCoq/metacoq/tree/coq-8.12/test-suite/safechecker_test.v) show example
+- The test-suite files [test-suite/erasure_test.v](https://github.com/MetaCoq/metacoq/tree/coq-8.13/test-suite/erasure_test.v)
+  and [test-suite/safechecker_test.v](https://github.com/MetaCoq/metacoq/tree/coq-8.13/test-suite/safechecker_test.v) show example
   uses (and current limitations of) the verified checker and erasure.
 
 
@@ -227,7 +227,7 @@ Copyright (c) 2018-2020 Danil Annenkov, Yannick Forster, Théo Winterhalter
 ```
 
 This software is distributed under the terms of the MIT license.
-See [LICENSE](https://github.com/MetaCoq/metacoq/tree/coq-8.12/LICENSE) for details.
+See [LICENSE](https://github.com/MetaCoq/metacoq/tree/coq-8.13/LICENSE) for details.
 
 
 

coq-metacoq-template.opam

@@ -1,7 +1,7 @@
 opam-version: "2.0"
 maintainer: "matthieu.sozeau@inria.fr"
 homepage: "https://metacoq.github.io/metacoq"
-dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.12"
+dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.13"
 bug-reports: "https://github.com/MetaCoq/metacoq/issues"
 authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
           "Simon Boulier <simon.boulier@inria.fr>"