merge changes from master that do not break 8.12

.github/workflows/docker-action.yml

@@ -0,0 +1,34 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - v8.12
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'coqorg/coq:8.12'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-paramcoq.opam'
+          custom_image: ${{ matrix.image }}
+          export: 'OPAMWITHTEST'
+        env:
+          OPAMWITHTEST: 'true'
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

.gitignore

@@ -1,6 +1,6 @@
 # Generated Makefile
-/Makefile.coq
-/Makefile.coq.conf
+Makefile.coq
+Makefile.coq.conf
 
 # Make dependencies
 *.d
@@ -38,3 +38,7 @@
 
 # coqpp generated file
 src/abstraction.ml
+
+# lia cache
+.lia.cache
+status

Makefile

@@ -1,14 +1,16 @@
-# -*- Makefile -*-
-.PHONY: coq clean
+all: Makefile.coq
+	@+$(MAKE) -f Makefile.coq all
 
-coq:: Makefile.coq
-	$(MAKE) -f Makefile.coq
+clean: Makefile.coq
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
 
-Makefile.coq: Make.cfg
-	coq_makefile -f Make.cfg -o Makefile.coq
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-distclean:
-	rm -f Makefile.coq Makefile.coq.conf Makefile.coq.bak .coqdeps.d
+force _CoqProject Makefile: ;
 
-install:
-	$(MAKE) -f Makefile.coq install
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
+
+.PHONY: all clean force

README.md

@@ -0,0 +1,127 @@
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
+# Paramcoq
+
+[![Docker CI][docker-action-shield]][docker-action-link]
+[![Contributing][contributing-shield]][contributing-link]
+[![Code of Conduct][conduct-shield]][conduct-link]
+[![Zulip][zulip-shield]][zulip-link]
+[![DOI][doi-shield]][doi-link]
+
+[docker-action-shield]: https://github.com/coq-community/paramcoq/workflows/Docker%20CI/badge.svg?branch=v8.12
+[docker-action-link]: https://github.com/coq-community/paramcoq/actions?query=workflow:"Docker%20CI"
+
+[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
+[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
+
+[conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg
+[conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md
+
+[zulip-shield]: https://img.shields.io/badge/chat-on%20zulip-%23c1272d.svg
+[zulip-link]: https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users
+
+
+[doi-shield]: https://zenodo.org/badge/DOI/10.4230/LIPIcs.CSL.2012.399.svg
+[doi-link]: https://doi.org/10.4230/LIPIcs.CSL.2012.399
+
+A Coq plugin providing commands for generating parametricity statements.
+Typical applications of such statements are in data refinement proofs.
+Note that the plugin is still in an experimental state - it is not very user
+friendly (lack of good error messages) and still contains bugs. But it
+is usable enough to "translate" a large chunk of the standard library.
+
+## Meta
+
+- Author(s):
+  - Chantal Keller (initial)
+  - Marc Lasson (initial)
+  - Abhishek Anand
+  - Pierre Roux
+  - Emilio Jesús Gallego Arias
+  - Cyril Cohen
+  - Matthieu Sozeau
+- Coq-community maintainer(s):
+  - Pierre Roux ([**@proux01**](https://github.com/proux01))
+- License: [MIT License](LICENSE)
+- Compatible Coq versions: The v8.12 branch tracks version 8.13 of Coq, see releases for compatibility with released versions of Coq.
+- Additional dependencies: none
+- Coq namespace: `Param`
+- Related publication(s):
+  - [Parametricity in an Impredicative Sort](https://hal.archives-ouvertes.fr/hal-00730913/) doi:[10.4230/LIPIcs.CSL.2012.399](https://doi.org/10.4230/LIPIcs.CSL.2012.399)
+
+## Building and installation instructions
+
+The easiest way to install the latest released version of Paramcoq
+is via [OPAM](https://opam.ocaml.org/doc/Install.html):
+
+```shell
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam install coq-paramcoq
+```
+
+To instead build and install manually, do:
+
+``` shell
+git clone https://github.com/coq-community/paramcoq.git
+cd paramcoq
+make   # or make -j <number-of-cores-on-your-machine> 
+make install
+```
+
+
+## Usage and Commands
+
+To load the plugin and make its commands available:
+```coq
+From Param Require Import Param.
+```
+
+The command scheme for named translations is:
+```
+Parametricity <ident> as <name> [arity <n>].
+```
+For example, the following command generates a translation named `my_param`
+of the constant or inductive `my_id` with arity 2 (the default):
+```coq
+Parametricity my_id as my_param.
+```
+
+The command scheme for automatically named translations is:
+```coq
+Parametricity [Recursive] <ident> [arity <n>] [qualified].
+```
+Such commands generate and name translations based on the given identifier.
+The `Recursive` option can be used to recursively translate all the constants
+and inductives which are used by the constant or inductive with the given
+identifier. The `qualified` option allows you to use a qualified default name
+for the translated constants and inductives. The default name then has the form
+`Module_o_Submodule_o_my_id` if the identifier `my_id` is declared in the
+`Module.Submodule` namespace.
+
+Instead of using identifiers, you can provide explicit terms to translate,
+according to the following command scheme:
+```coq
+Parametricity Translation <term> [as <name>] [arity <n>].
+```
+This defines a new constant containing the parametricity translation of
+the given term.
+
+To recursively translate everything in a module:
+```coq
+Parametricity Module <module_path>.
+```
+
+When translating terms containing section variables or axioms,
+it may be useful to declare a term to be the translation of a constant:
+```coq
+Realizer <constant_or_variable> [as <name>] [arity <n>] := <term>.
+```
+
+Note that translating a term or module may lead to proof obligations (for some
+fixpoints and opaque terms if you did not import `ProofIrrelevence`). You need to
+declare a tactic to solve such proof obligations:
+```coq
+[Global|Local] Parametricity Tactic := <tactic>.
+```

Make.cfg → _CoqProject

@@ -1,3 +1,4 @@
+-R theories Param
 -R src Param
 -I src
 src/debug.ml
@@ -6,3 +7,4 @@ src/relations.ml
 src/declare_translation.ml
 src/abstraction.mlg
 src/paramcoq.mlpack
+theories/Param.v

coq-paramcoq.opam

@@ -1,40 +1,42 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
 opam-version: "2.0"
-version: "1.1.2+coq8.12"
 maintainer: "Pierre Roux <pierre.roux@onera.fr>"
+version: "8.12.dev"
 
 homepage: "https://github.com/coq-community/paramcoq"
 dev-repo: "git+https://github.com/coq-community/paramcoq.git"
 bug-reports: "https://github.com/coq-community/paramcoq/issues"
 license: "MIT"
 
+synopsis: "Plugin for generating parametricity statements to perform refinement proofs"
+description: """
+A Coq plugin providing commands for generating parametricity statements.
+Typical applications of such statements are in data refinement proofs.
+Note that the plugin is still in an experimental state - it is not very user
+friendly (lack of good error messages) and still contains bugs. But it
+is usable enough to "translate" a large chunk of the standard library."""
+
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.12" & < "8.13~"}
+  "coq" {>= "8.12" & < "8.13" }
 ]
 
 tags: [
+  "category:Miscellaneous/Coq Extensions"
   "keyword:paramcoq"
   "keyword:parametricity"
   "keyword:ocaml module"
-  "category:Miscellaneous/Coq Extensions"
   "logpath:Param"
 ]
 authors: [
-  "Chantal Keller (Inria, École polytechnique)"
-  "Marc Lasson (ÉNS de Lyon)"
+  "Chantal Keller"
+  "Marc Lasson"
   "Abhishek Anand"
   "Pierre Roux"
   "Emilio Jesús Gallego Arias"
   "Cyril Cohen"
   "Matthieu Sozeau"
 ]
-synopsis: "Plugin for generating parametricity statements to perform refinement proofs"
-description: """
-The plugin is still in an experimental state. It is not very user
-friendly (lack of good error messages) and still contains bugs. But is
-useable enough to "translate" a large chunk of standard library."""
-url {
-  src: "https://github.com/coq-community/paramcoq/archive/v1.1.2+coq8.7.tar.gz"
-  checksum: "sha256=48fcb716c00d52802a9596ee396eab9af7f368da6afebdbb9cf67738ae133b97"
-}

dune-project

@@ -0,0 +1,3 @@
+(lang dune 2.5)
+(using coq 0.2)
+(name paramcoq)