paramcoq

paramcoq copied to clipboard

ppedrot

Typo

2

In src/parametricity, you should s/environement/environment/g: ``` --- paramcoq.orig/src/parametricity.ml +++ paramcoq/src/parametricity.ml @@ -604,7 +604,7 @@ compose_prod_assum (lift_rel_context (nfun * order) ft_R) (substl sub bk_R)) ftbk_R in - (* env_rec is the...

SnarkBoojum

Applying the parametricity techniques to the generation of Boolean equality

12

Hi, I made recently an experiment of using parametricity techniques in Coq to automatically generate a Boolean equality associated to an inductive type as an alternative to the ad hoc...

herbelin

Proof obligations, even on closed programs

4

Based on the description of the plugin in [1], I expected it to not need any user input when translating closed terms. However, sometimes, it leaves me with strange proof...

aa755

Add Coq Nix Toolbox-based CI to test CoqEAL.

1

Closes #74.

Zimmi48

Nix CI with caching and checking of CoqEAL

1

This is a memento that we would eventually like to have CI for paramcoq using the [Nix Toolbox](https://github.com/coq-community/coq-nix-toolbox) and Nix Action that incorporates the following features: - caching using the...

palmskog

Proof obligations generated, but not in the proof mode

1

The `Parametricity Recursive` command says "The parametricity tactic generated generated proof obligations. Please prove them and end your proof with 'Parametricity Done'". But it does not open the proof mode....

pi8027

strange warning from coqdep

2

Hi, I am writing a library which uses paramcoq (installed with opam). At compile-time, I get a warning: *** Warning: in file ./power/Addition_Chains.v, declared ML module paramcoq has not been...

Casteran