aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/recdef.mli
Commit message (Expand)AuthorAge
* Remove dead code from funind.Gravatar Maxime Dénès2018-01-24
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Removing Proof_type from the API.Gravatar Pierre-Marie Pédrot2017-06-16
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* 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