aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/auto_ind_decl.mli
Commit message (Expand)AuthorAge
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-01-23
|\
| * Excluding explicitly coinductive types in Scheme Equality (#5284).Gravatar Hugo Herbelin2016-12-23
* | Fix bug #5069: Scheme Equality gives anomalies in sections.Gravatar Pierre-Marie Pédrot2016-10-02
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fixing bug #3736 (anomaly instead of error/warning/silence onGravatar Hugo Herbelin2015-07-27
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Updating headers.Gravatar herbelin2012-08-08
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Added the automatic generation of the boolean equality if possible and theGravatar vsiles2007-10-05