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
...
*
- 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
*
Affichage des dir_path vide
herbelin
2001-09-19
*
Romega/names/Makefile
mohring
2001-09-18
*
erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies
barras
2001-09-04
*
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 d'espace dans les règles d'affichage des infix si des lettres figurent...
herbelin
2001-01-31
*
Ajout alias mutual_inductive_path = section_path
herbelin
2001-01-27
*
Alias variable_path
herbelin
2000-12-25
*
Le bon choix, c'est finalement identifier = string
herbelin
2000-12-15
*
Mise en place d'un module Ident avec test de l'efficacité quand identifier=s...
herbelin
2000-12-15
*
Mini-nettoyage noms longs
herbelin
2000-12-05
[prev]
[next]