Participants: Pierre Boutillier, Pierre Courtieu, Hugo Herbelin, Pierre Letouzey, Ludovic Patey, Yann RĂ©gis-Gianas, Arnaud Spiwack, Enrico Tassi.

Points discussed for integration to Coq 8.5

New-tacticals (Arnaud)


, ..., ++, +++, ... **, ***, ... (but how to hack the lexer for that, in particular in coqide?)

Asynchronous lazy evaluation of commands (Enrico)

Full polymorphism of universes (Matthieu)

Ad hoc representation of projections in the code (Matthieu)

Hack for not doing intensive computations both at proof time and qed time (Enrico)

Coqdoc (Yann)

All points discussed are agreed for integration to Coq 8.5

Miscellaneous discussions

Reduction of vo size with modules (Letouzey)

Obtained by represention "M:=N" in an algebraic way in declaremods.ml

Introduction of a proper intropattern notation for injecting an equality on the fly (Hugo)

Syntax "[=pat1 ... patn]" has been approved

Compilation of user contributions and test-suite

Pierre Boutillier reminds that several contribs and tests fail to compile in 8.3, 8.4 and trunk

CoqDevelopment/CRGTCoq20130709 (last edited 22-07-2013 16:52:20 by oumix)

Cocorico!WikiLicense