Pierre Castéran

Issue with python_select while installing the Coq Platform (on macOS with MacPorts)

5

We have an issue trying to install Coq Platform 2022.04.1 on macOS 12.3.1 with MacPorts. We get the following error message. It seems like the issue is with MacPorts itself,...

Changes for Coq 8.13.0

3

@ybertot @palmskog I will do the following changes: Fix the warnings about Hints locallity attributes and unused match variables. Remove the Admitted in chap7.v (replace with small proofs). They prevented...

Alectryon displays local definitions (with set, pose) as declarations

3

In the following proof, `alectryon AlectryonIssue.v --backend latex` builds a document where the variable `z` is presented as a simple declaration `z: nat` and not `z := Nat.max x y...

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...

Mentionned as https://github.com/cpitclaudel/alectryon/issues/94