aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/inductive.mli
Commit message (Expand)AuthorAge
* [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
* [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
| | * Add a flag to deactivate guard checking in the kernel.Gravatar Arnaud Spiwack2015-06-26
| |/ |/|
* | Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-18
| * Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Refining match subterm and commutative cut rules. The parameters that areGravatar Maxime Dénès2014-07-22
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Delayed the computation of parameters in sort polymorphism ofGravatar herbelin2013-05-14
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Extraction: forbid Prop-polymorphism of inductives when extracting to OcamlGravatar letouzey2011-07-04
* 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
* Added printing of recursive notations in cases pattern (supported by wish 2248).Gravatar herbelin2010-06-14
* Some ocamldoc comments + Fixing name of .coqrc.version file in refmanGravatar pboutill2010-05-18
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* introduced lazy computation of size info in the guard conditionGravatar barras2010-03-11
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Fixing bug #2139 (kernel-based test of well-formation of eliminationGravatar herbelin2009-07-15
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
* bug condition de gardeGravatar barras2006-12-08
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* correction bugs de condition de garde (fix + cofix)Gravatar barras2006-05-12
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29