Frédéric Blanqui

icon indicating a website link https://blanqui.gitlabpages.inria.fr/

icon company INRIA icon location Gif-sur-Yvette, France

Results 112 issues of Frédéric Blanqui

Problem with some notation

Hi. PG gets frozen with the following file when we reach the line 3: ``` Axiom Ninterval: nat -> nat -> Prop. Notation "[ n '....' m ]" := (Ninterval...

Error: The compilation of rocq-hierarchy-builder.1.9.1 failed at "make build".

4 comment

Hi. I get a compilation error with opam with coq 8.19: ``` - install atd 2.16.0 [required by atdgen, atdts] - install atdgen 2.15.0 [required by elpi] - install atdgen-runtime...