aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/recdef.mli
Commit message (Expand)AuthorAge
* Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Modulification of identifierGravatar ppedrot2012-12-14
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* New version of recdef :Gravatar jforest2012-03-01