aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/recdef.mli
Commit message (Expand)AuthorAge
* 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