index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
inductive.mli
Commit message (
Expand
)
Author
Age
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
[api] Remove yet another type alias.
Emilio Jesus Gallego Arias
2017-12-09
*
[api] Remove aliases of `Evar.t`
Emilio Jesus Gallego Arias
2017-11-26
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Moving the typing_flags to the environment.
Pierre-Marie Pédrot
2016-06-18
*
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-06-16
|
\
|
*
Assume totality: dedicated type rather than bool
Arnaud Spiwack
2016-06-14
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
\
|
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
|
|
*
Add a flag to deactivate guard checking in the kernel.
Arnaud Spiwack
2015-06-26
|
|
/
|
/
|
*
|
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-18
|
*
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-17
|
/
*
Update headers.
Maxime Dénès
2015-01-12
*
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-28
*
"allows to", like "allowing to", is improper
Jason Gross
2014-08-25
*
Move to a representation of universe polymorphic constants using indices for ...
Matthieu Sozeau
2014-08-03
*
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-08-01
*
Refining match subterm and commutative cut rules. The parameters that are
Maxime Dénès
2014-07-22
*
- Fix hashing of levels to get the "right" order in universe contexts etc...
Matthieu Sozeau
2014-06-04
*
Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.
Matthieu Sozeau
2014-05-06
*
Initial work on reintroducing old-style polymorphism for compatibility (the s...
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Delayed the computation of parameters in sort polymorphism of
herbelin
2013-05-14
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Modulification of identifier
ppedrot
2012-12-14
*
Updating headers.
herbelin
2012-08-08
*
Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml
letouzey
2011-07-04
*
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
*
Added printing of recursive notations in cases pattern (supported by wish 2248).
herbelin
2010-06-14
*
Some ocamldoc comments + Fixing name of .coqrc.version file in refman
pboutill
2010-05-18
*
Applicative commutative cuts in Fixpoint guard condition
pboutill
2010-05-18
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
introduced lazy computation of size info in the guard condition
barras
2010-03-11
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Fixing bug #2139 (kernel-based test of well-formation of elimination
herbelin
2009-07-15
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
Correction d'une incohérence de typage des inductifs polymorphes: les
herbelin
2008-07-25
*
bug condition de garde
barras
2006-12-08
*
Compatibilité du polymorphisme de constantes avec les sections.
herbelin
2006-10-29
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
- Ajout d'un cast vm dans la syntaxe : x <: t
bgregoir
2006-07-22
*
- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites
herbelin
2006-05-28
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
correction bugs de condition de garde (fix + cofix)
barras
2006-05-12
[next]