aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/recdef.mli
Commit message (Expand)AuthorAge
* Merge branch v8.6 into trunkGravatar Hugo Herbelin2017-04-22
|\
| * Solving first problem in bug #4306. TO DO : solve the let in problemGravatar Julien Forest2017-04-04
* | 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