Clément Pit-Claudel

monospacifier. Convert variable-pitch fonts to monospace (useful for unicode and indentation-friendly programming)

company-coq. A Coq IDE build on top of Proof General's Coq mode

alectryon. A collection of tools for writing technical documents that mix Rocq code and prose.

biblio.el. Browse and import bibliographic references from CrossRef, DBLP, HAL, arXiv, Dissemin, and doi.org from Emacs

z3.wasm. WASM builds of the Z3 SMT solver

academic-poster-template. An HTML+CSS template for making more accessible posters

quick-peek. Quick-peek inline-window library for Emacs

easy-escape. Improve readability of escape characters in ELisp regular expressions

fstar.js. F* running in the browser

dBoost. TeX

esh. Use Emacs to highlight source code listings in LaTeX and HTML documents!

compact-docstrings. Shrink blank lines in docstrings and doc comments

elcoq. Experiments with SerAPI in Emacs

cvc4.js. asm.js and WebAssembly ports of the CVC4 SMT solver

coq-rst. An experiment in porting Coq's manual to reStructuredText

synquid-emacs. Edit Synquid files in Emacs!

presenter-mode. Who needs PowerPoint?

FStar. An ML-like language aimed at program verification

rocq. Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.