aboutsummaryrefslogtreecommitdiff
path: root/toplevel/auto_ind_decl.mli
AgeCommit message (Expand)Author
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2017-01-23Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-12-23Excluding explicitly coinductive types in Scheme Equality (#5284).Hugo Herbelin
2016-10-02Fix bug #5069: Scheme Equality gives anomalies in sections.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-07-27Fixing bug #3736 (anomaly instead of error/warning/silence onHugo Herbelin
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-08-08State Transaction Machinegareuselesinge
2013-04-29Merging Context and Sign.ppedrot
2012-08-08Updating headers.herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2007-10-05 Added the automatic generation of the boolean equality if possible and thevsiles
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:07:05 +0000