This place is dedicated to small inversions for Coq and Rocq.

# PBSI
The more recent development is called PBSI (proxy-based small inversions).
It is largely automated in a tool mainly developed by Basile Gros,
during its PhD under the supervision of Pierre Corbineau and Jean-François Monin.
This tool is available here:

<https://github.com/BasileGros/proxy-based-small-inversions>

# History (sketch)
* 2010: first version published at the Coq Workshop
* 2013: second version published at ITP, based on continuations
* 2015-now: unpublished version used in teaching, based on auxiliary algebraic types.
  Became basic PBSI.
* 2026: PBSI published at LPAR, including dependent PBSI that facilitate
  the development of Rocq programs with dependent types and of proofs over them.

Coucou