update meta and readme

README.md

@@ -23,19 +23,30 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [doi-shield]: https://zenodo.org/badge/DOI/10.5281/zenodo.10492403.svg
 [doi-link]: https://doi.org/10.5281/zenodo.10492403
 
-Trocq is a modular parametricity plugin for Coq. It 
-can be used to achieve proof transfer by both translating a user goal into another, related,
-variant, and computing a proof that proves the corresponding implication.
-
-The plugin features a hierarchy of structures on relations, whose instances are computed from registered user-defined proof via parametricity. This hierarchy ranges from structure-less relations to an original formulation of type
-equivalence. The resulting framework generalizes [raw parametricity](https://arxiv.org/abs/1209.6336), 
-[univalent parametricity](https://arxiv.org/abs/1209.6336) and
-[CoqEAL](https://github.com/coq-community/coqeal), and includes them in a unified framework.
-
-The plugin computes a parametricity translation "à la carte", by performing a fine-grained analysis of the requires properties for a given proof of relatedness. In particular, it is able to prove implications without resorting to full-blown type equivalence, allowing this way to perform
-proof transfer without necessarily pulling in the univalence axiom. 
-
-The plugin is implemented in Coq-Elpi and the code of the parametricity translation is fairly close to a pen-and-paper sequent-style presentation.
+Trocq is a modular parametricity plugin for Coq. It can be used to
+achieve proof transfer by both translating a user goal into another,
+related, variant, and computing a proof that proves the corresponding implication.
+
+The plugin features a hierarchy of structures on relations, whose
+instances are computed from registered user-defined proof via
+parametricity. This hierarchy ranges from structure-less relations
+to an original formulation of type equivalence. The resulting
+framework generalizes [raw
+parametricity](https://arxiv.org/abs/1209.6336), [univalent
+parametricity](https://doi.org/10.1145/3429979) and
+[CoqEAL](https://github.com/coq-community/coqeal), and includes them
+in a unified framework.
+
+The plugin computes a parametricity translation "à la carte", by
+performing a fine-grained analysis of the requires properties for a
+given proof of relatedness. In particular, it is able to prove
+implications without resorting to full-blown type equivalence,
+allowing this way to perform proof transfer without necessarily
+pulling in the univalence axiom.
+
+The plugin is implemented in Coq-Elpi and the code of the
+parametricity translation is fairly close to a pen-and-paper
+sequent-style presentation.
 
 ## Meta
 
@@ -58,26 +69,28 @@ The plugin is implemented in Coq-Elpi and the code of the parametricity translat
 
 ## Building and installation instructions
 
-Trocq is a still a prototype. In particular, it depends on a [custom version](https://github.com/ecranceMERCE/coq-elpi/tree/strat) of Coq-Elpi.
-It is not yet packaged in Opam or Nix.
+Trocq is a still a prototype. In particular, it depends on a [custom
+version](https://github.com/ecranceMERCE/coq-elpi/tree/strat) of
+Coq-Elpi.  It is not yet packaged in Opam or Nix.
 
-There are however three ways to experiment with it,
-all documented in the [INSTALL.md file](INSTALL.md).
+There are however three ways to experiment with it, all documented
+in the [INSTALL.md file](INSTALL.md).
 
 ## Documentation
 
 See the [tutorial](artifact-doc/TUTORIAL.md) for concrete use cases.
 
 In short, the plugin provides a tactic:
 - `trocq` (without arguments) which attempts to run a translation on
-a given goal, using the information provided by the user with the
-commands described below.
+  a given goal, using the information provided by the user with the
+  commands described below.
 
 And three commands:
-- `Trocq Use t` to use a translation `t` during the subsequent calls to
-the tactic `trocq`.
+- `Trocq Use t` to use a translation `t` during the subsequent calls
+  to the tactic `trocq`.
 - `Trocq Register Univalence u` to declare a univalence axiom `u`.
-- `Trocq Register Funext fe` to declare a function extensionality axiom `fe`.
+- `Trocq Register Funext fe` to declare a function extensionality
+  axiom `fe`.
 
 
 ## ESOP 2024 artifact documentation

coq-trocq.opam

@@ -12,27 +12,30 @@ license: "LGPL-3.0-or-later"
 
 synopsis: "A modular parametricity plugin for proof transfer in Coq"
 description: """
-Trocq is a prototype of a modular parametricity plugin for Coq, aiming
-to perform proof transfer by translating the goal into an associated
-goal featuring the target data structures as well as a rich
-parametricity witness from which a function justifying the goal
-substitution can be extracted.
-
-The plugin features a hierarchy of parametricity witness types,
-ranging from structure-less relations to a new formulation of type
-equivalence, gathering several pre-existing parametricity
-translations, including
-[univalent parametricity](https://doi.org/10.1145/3429979) and
-[CoqEAL](https://github.com/coq-community/coqeal), in the same framework.
-
-This modular translation performs a fine-grained analysis and
-generates witnesses that are rich enough to preprocess the goal yet
-are not always a full-blown type equivalence, allowing to perform
-proof transfer with the power of univalent parametricity, but trying
-not to pull in the univalence axiom in cases where it is not required.
-
-The translation is implemented in Coq-Elpi and features transparent
-and readable code with respect to a sequent-style theoretical presentation."""
+Trocq is a modular parametricity plugin for Coq. It can be used to
+achieve proof transfer by both translating a user goal into another,
+related, variant, and computing a proof that proves the corresponding implication.
+
+The plugin features a hierarchy of structures on relations, whose
+instances are computed from registered user-defined proof via
+parametricity. This hierarchy ranges from structure-less relations
+to an original formulation of type equivalence. The resulting
+framework generalizes [raw
+parametricity](https://arxiv.org/abs/1209.6336), [univalent
+parametricity](https://doi.org/10.1145/3429979) and
+[CoqEAL](https://github.com/coq-community/coqeal), and includes them
+in a unified framework.
+
+The plugin computes a parametricity translation "à la carte", by
+performing a fine-grained analysis of the requires properties for a
+given proof of relatedness. In particular, it is able to prove
+implications without resorting to full-blown type equivalence,
+allowing this way to perform proof transfer without necessarily
+pulling in the univalence axiom.
+
+The plugin is implemented in Coq-Elpi and the code of the
+parametricity translation is fairly close to a pen-and-paper
+sequent-style presentation."""
 
 build: [make "-j%{jobs}%"]
 install: [make "install"]

meta.yml

@@ -11,27 +11,30 @@ synopsis: >-
   A modular parametricity plugin for proof transfer in Coq
 
 description: |-
-  Trocq is a prototype of a modular parametricity plugin for Coq, aiming
-  to perform proof transfer by translating the goal into an associated
-  goal featuring the target data structures as well as a rich
-  parametricity witness from which a function justifying the goal
-  substitution can be extracted.
-
-  The plugin features a hierarchy of parametricity witness types,
-  ranging from structure-less relations to a new formulation of type
-  equivalence, gathering several pre-existing parametricity
-  translations, including
-  [univalent parametricity](https://doi.org/10.1145/3429979) and
-  [CoqEAL](https://github.com/coq-community/coqeal), in the same framework.
-
-  This modular translation performs a fine-grained analysis and
-  generates witnesses that are rich enough to preprocess the goal yet
-  are not always a full-blown type equivalence, allowing to perform
-  proof transfer with the power of univalent parametricity, but trying
-  not to pull in the univalence axiom in cases where it is not required.
-
-  The translation is implemented in Coq-Elpi and features transparent
-  and readable code with respect to a sequent-style theoretical presentation.
+  Trocq is a modular parametricity plugin for Coq. It can be used to
+  achieve proof transfer by both translating a user goal into another,
+  related, variant, and computing a proof that proves the corresponding implication.
+
+  The plugin features a hierarchy of structures on relations, whose
+  instances are computed from registered user-defined proof via
+  parametricity. This hierarchy ranges from structure-less relations
+  to an original formulation of type equivalence. The resulting
+  framework generalizes [raw
+  parametricity](https://arxiv.org/abs/1209.6336), [univalent
+  parametricity](https://doi.org/10.1145/3429979) and
+  [CoqEAL](https://github.com/coq-community/coqeal), and includes them
+  in a unified framework.
+
+  The plugin computes a parametricity translation "à la carte", by
+  performing a fine-grained analysis of the requires properties for a
+  given proof of relatedness. In particular, it is able to prove
+  implications without resorting to full-blown type equivalence,
+  allowing this way to perform proof transfer without necessarily
+  pulling in the univalence axiom.
+
+  The plugin is implemented in Coq-Elpi and the code of the
+  parametricity translation is fairly close to a pen-and-paper
+  sequent-style presentation.
 
 publications:
 - pub_url: https://hal.science/hal-04177913/document
@@ -98,30 +101,30 @@ categories:
 build: |-
   ## Building and installation instructions
 
-  As Trocq is a prototype, it is currently unreleased, and depends on a
-  [custom version](https://github.com/ecranceMERCE/coq-elpi/tree/strat)
-  of Coq-Elpi. It is not yet packaged in Opam or Nix, but will be in
-  the near future.
-
-  There are however three ways to develop it and experiment with it,
-  they are documented in the [INSTALL.md file](INSTALL.md).
+  Trocq is a still a prototype. In particular, it depends on a [custom
+  version](https://github.com/ecranceMERCE/coq-elpi/tree/strat) of
+  Coq-Elpi.  It is not yet packaged in Opam or Nix.
 
+  There are however three ways to experiment with it, all documented
+  in the [INSTALL.md file](INSTALL.md).
 
 documentation: |-
   ## Documentation
 
-  For now, there is one tactic:
+  See the [tutorial](artifact-doc/TUTORIAL.md) for concrete use cases.
+
+  In short, the plugin provides a tactic:
   - `trocq` (without arguments) which attempts to run a translation on
-  a given goal, using the information provided by the user with the
-  commands described below.
+    a given goal, using the information provided by the user with the
+    commands described below.
 
   And three commands:
-  - `Trocq Use t` to use a translation `t` during the subsequent calls to
-  the tactic `trocq`.
+  - `Trocq Use t` to use a translation `t` during the subsequent calls
+    to the tactic `trocq`.
   - `Trocq Register Univalence u` to declare a univalence axiom `u`.
-  - `Trocq Register Funext fe` to declare a function extensionality axiom `fe`.
+  - `Trocq Register Funext fe` to declare a function extensionality
+    axiom `fe`.
 
-  See the [tutorial](artifact-doc/TUTORIAL.md) for concrete usecases.
 
   ## ESOP 2024 artifact documentation