index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
cooking.ml
Age
Commit message (
Expand
)
Author
2009-10-21
This big commit addresses two problems:
soubiran
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-08-06
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2008-04-30
Réutilisation de l'infrastructure pour le polymorphisme d'univers des
herbelin
2007-12-05
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-04-25
New keyword "Inline" for Parameters and Axioms for automatic
soubiran
2006-10-30
dependences
barras
2006-10-29
Compatibilité du polymorphisme de constantes avec les sections.
herbelin
2006-10-28
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-04-27
Standardisation nom option_app en option_map
herbelin
2005-02-18
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2004-11-16
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-10-20
COMMITED BYTECODE COMPILER
barras
2004-07-16
Nouvelle en-tête
herbelin
2002-10-07
Lazy manuelles dans le code
coq
2002-10-05
Lazy experimentale temporaire...
coq
2002-08-02
Modules dans COQ\!\!\!\!
coq
2001-12-13
compat ocaml 3.03
filliatr
2001-11-12
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-05
GROS COMMIT:
barras
2001-10-09
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-09-21
repare la perte d'opacite a la fermeture de section
barras
2001-09-09
Mécanisme pour faire remonter les contraintes de typage sur les variables de...
herbelin
2001-08-10
Parsing
herbelin
2001-07-21
Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...
herbelin
2001-05-23
amelioration des messages d'erreurs vis a vis des evars
barras
2001-03-15
entetes
filliatr
2001-02-14
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2000-11-27
On déplie les locaux dans les types plutôt que de les quantifier par un Let
herbelin
2000-11-20
Tables séparées pour chaque type de global
herbelin
2000-11-06
nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...
filliatr