index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
names.ml
Commit message (
Expand
)
Author
Age
*
compatibility <3.12 (Map.exists Map.singleton)
pboutill
2011-02-11
*
Make simpl use the proper constant when folding (mutual) fixpoints
letouzey
2011-01-27
*
Fixing printing of module_path names (was using a debugging
herbelin
2010-10-03
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Names: remove obsolete mod_self_id
letouzey
2010-06-23
*
Added a few informations about file lineages (for the most part in kernel)
herbelin
2010-05-09
*
After the approval of Bruno, here the patch for the checker.
soubiran
2010-04-29
*
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
*
- coq_makefile: target install now respects the original tree structure
herbelin
2008-12-24
*
Report des commits 11417 et 11437 de la v8.2
soubiran
2008-10-15
*
Autour du parsing:
herbelin
2008-07-15
*
Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...
notin
2008-06-25
*
- Cleanup parsing of binders, reducing to a single production for all
msozeau
2008-05-11
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
*
- Parameterize unification by two sets of transparent_state, one for open
msozeau
2008-04-21
*
suite 10790 (identificateurs)
herbelin
2008-04-14
*
Bugs, nettoyage, et améliorations diverses
herbelin
2008-04-13
*
Nettoyage de code en vue de la release. Plus de Warning: Unused
aspiwack
2007-12-18
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
Fixed the pseudo-cicularity problem due to the with operator on Module Type.
soubiran
2007-02-21
*
modifications des messages d'erreurs renvoyés lors de la comparaison
soubiran
2007-01-24
*
Modification de add_glob (support des modules dans Coqdoc)
notin
2006-05-23
*
Suppression résidus code v7 et traducteur
herbelin
2006-01-11
*
Moved Indmap and ConstrMap from Libnames to Names for use in Cooking
herbelin
2005-02-18
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Nouvelle en-tête
herbelin
2004-07-16
*
Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans coqt...
herbelin
2004-03-28
*
*** empty log message ***
barras
2003-03-12
*
*** empty log message ***
courant
2003-01-31
*
id_of_msid en plus
letouzey
2003-01-22
*
Corrections de gestion des univers et modules + meilleure gestions des noms...
coq
2002-12-09
*
des Set et des Map en plus
letouzey
2002-12-05
*
Corrige un bug de composition de substitutions
coq
2002-12-04
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Hash-consing pour kernel_name
herbelin
2002-09-29
*
Pretty-printing preliminaire des modules, commandes
coq
2002-08-19
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
reparation de Locate
barras
2001-11-29
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
GROS COMMIT:
barras
2001-11-05
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...
herbelin
2001-10-12
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Transparent
barras
2001-09-20
*
Romega
mohring
2001-09-20
[next]