index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
entries.ml
Commit message (
Expand
)
Author
Age
*
[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
*
More precise type for universe entries.
Pierre-Marie Pédrot
2017-07-26
*
[api] Put modules in order in API.{mli,ml}
Emilio Jesus Gallego Arias
2017-07-25
*
Cleared a purely declarative .ml file and moved its interface to intf/
ppedrot
2012-10-23
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Proof using ...
gareuselesinge
2011-12-12
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
A fine-grain control of inlining at functor application via priority levels
letouzey
2011-01-31
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
Ajout des alias de module dans le noyau.
soubiran
2008-03-14
*
Beaoucoup de changements dans la representation interne des modules.
soubiran
2008-02-01
*
New keyword "Inline" for Parameters and Axioms for automatic
soubiran
2007-04-25
*
Removed some useless code in mod_typing that was redundant with safe_typing.
soubiran
2007-02-21
*
MAJ documentation en syntaxe v8
herbelin
2006-03-18
*
Types inductifs parametriques
mohring
2005-11-02
*
Construct "T with (Definition|Module) id := c" generalized to
sacerdot
2005-01-13
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Nouvelle en-tête
herbelin
2004-07-16
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
La notation 'with'. L'interpretation - version preliminaire
coq
2002-08-19
*
Modules dans COQ\!\!\!\!
coq
2002-08-02