index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
names.mli
Commit message (
Expand
)
Author
Age
*
Names: remove obsolete mod_self_id
letouzey
2010-06-23
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
After the approval of Bruno, here the patch for the checker.
soubiran
2010-04-29
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Names.mli: double declaration of mind_modpath
letouzey
2010-04-16
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Report des commits 11417 et 11437 de la v8.2
soubiran
2008-10-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
*
- Parameterize unification by two sets of transparent_state, one for open
msozeau
2008-04-21
*
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
*
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
*
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
*
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
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
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
*
Compatibilté make doc
herbelin
2001-09-20
*
Parsing
herbelin
2001-08-10
*
Ajout add_prefix/add_suffix
herbelin
2001-08-01
*
entetes
filliatr
2001-03-15
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
ident au lieu de string pour le nom de base de qualid
herbelin
2001-02-16
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
Ajout alias mutual_inductive_path = section_path
herbelin
2001-01-27
*
Alias variable_path
herbelin
2000-12-25
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Mini-nettoyage noms longs
herbelin
2000-12-05
*
Ajout d'un test pour vérifier qu'on a affaire à un ident
herbelin
2000-11-29
[next]