index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
auto_ind_decl.mli
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2017-01-23
|
\
|
*
Excluding explicitly coinductive types in Scheme Equality (#5284).
Hugo Herbelin
2016-12-23
*
|
Fix bug #5069: Scheme Equality gives anomalies in sections.
Pierre-Marie Pédrot
2016-10-02
|
/
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Fixing bug #3736 (anomaly instead of error/warning/silence on
Hugo Herbelin
2015-07-27
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Update headers.
Maxime Dénès
2015-01-12
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Updating headers.
herbelin
2012-08-08
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Added the automatic generation of the boolean equality if possible and the
vsiles
2007-10-05