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
*
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
*
Prise en compte de noms absolus dans la nametab
herbelin
2000-11-26
*
Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_sp
herbelin
2000-11-23
*
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...
herbelin
2000-11-22
*
implicites manuels
filliatr
2000-11-21
*
Introduction constant_path = section_path
herbelin
2000-11-20
*
Nettoyage Names suite
herbelin
2000-11-07
*
Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...
herbelin
2000-11-06
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
modifs pour premiere edition de liens
filliatr
1999-12-02
[next]