In this repository the Lift function is defined. This function is implemented in Mtac2 for Coq, and is now working with Coq 8.11 and 8.10.2 at least.

The actual function can be found at curry.v.

The actual example which generalizes the list_max_nat which returns the max element of a list of nat, can be found in example.v

In devel some old files are located, but also concept.v contains the work on notation for automation.