aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declare.mli
Commit message (Expand)AuthorAge
* Hopefully better names to constructors of internal_flag, as discussedGravatar Hugo Herbelin2015-09-23
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Update headers.Gravatar Maxime Dénès2015-01-12
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* 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
* ind_tables: properly handling side effectsGravatar gareuselesinge2013-08-30
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Use definition_entry to declare local definitionsGravatar gareuselesinge2013-05-09
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Updating headers.Gravatar herbelin2012-08-08
* Rely on kernel to know if a name is already used so as to be consistent with it.Gravatar herbelin2011-10-08
* * removed declare_constant and declare_internal_constant Gravatar vsiles2010-09-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Backtrack on the forced discharge of type class variables introducedGravatar msozeau2009-09-14
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
* DISCLAIMERGravatar puech2009-01-17
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* Changement des named_contextGravatar gregoire2005-12-02
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* Export de l'information si un inductive est un record ou non (pour xml)Gravatar herbelin2004-03-31
* Distinction entre declarations internes (p.ex. _subproof) et declarations uti...Gravatar herbelin2004-03-30
* Memorisation du type de variable (Hyp or Var)Gravatar herbelin2004-03-26
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...Gravatar herbelin2003-09-12
* Petit netoyage des open's et commentairesGravatar coq2002-12-16
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Suppression automatique du corps des définitions locales opaques dansGravatar herbelin2002-08-17
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Déplacement/renommage de Class.stre_max en Declare.strength_minGravatar herbelin2002-04-16