aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/recdef.mli
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2012-12-14Modulification of identifierppedrot
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-03-01New version of recdef :jforest