index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
class.ml
Commit message (
Expand
)
Author
Age
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-06
*
Réorganisation de la structure interne des types de déclarations (decl_kinds)
herbelin
2006-01-28
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Complétion commit précédent
herbelin
2004-11-29
*
Réduire pour trouver l'arité d'une classe
herbelin
2004-11-26
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Nouvelle en-tête
herbelin
2004-07-16
*
Recherche de la source à partir de la gauche pour gérer des cas comme 'Coer...
herbelin
2004-06-02
*
test de conversion laissait echapper exception NotConvertible
barras
2004-05-14
*
MAJ messages d'erreurs en accord avec la doc
herbelin
2003-12-20
*
Déplacement d'un morceau de Declare
herbelin
2003-09-12
*
Tables logarithmiques pour les coercions + nettoyage
herbelin
2003-06-08
*
*** empty log message ***
barras
2003-03-12
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Que des niveaux d'univers frais dans le type des constantes globales
herbelin
2002-09-29
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Déplacement/renommage de Class.stre_max en Declare.strength_min
herbelin
2002-04-16
*
compat ocaml 3.03
filliatr
2001-12-13
*
Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant
herbelin
2001-11-20
*
Code mort
herbelin
2001-11-20
*
Nettoyage coercions et classes
herbelin
2001-11-09
*
GROS COMMIT:
barras
2001-11-05
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Transparent
barras
2001-09-20
*
Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...
herbelin
2001-09-19
*
Suppression du message d'erreur si une coercion mettant en jeu des locaux n'e...
herbelin
2001-09-18
*
Bug discharge d'une déclaration de coercion pour une constante non définie ...
herbelin
2001-09-18
*
Parsing
herbelin
2001-08-10
*
Débogage discharge des coercions; nettoyage
herbelin
2001-07-05
*
entetes
filliatr
2001-03-15
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Restructuration de classops; évolution en une version mieux intégrée au re...
herbelin
2001-02-05
*
Bug lié au discharge
herbelin
2001-01-31
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Bug Identity Coercion
herbelin
2001-01-18
*
Ajout du Let pour le langage de tactiques
delahaye
2000-12-29
*
Un nom long pour les variables de section qui font classe ou coercion; réorg...
herbelin
2000-12-25
*
caractere opaque des constantes repris en compte
filliatr
2000-12-04
*
Suppression cast inutile
herbelin
2000-11-29
*
Remplacement de certains sp_of_id par des locate
herbelin
2000-11-26
*
Informations inutiles
herbelin
2000-11-23
*
Mieux à sa place dans toplevel
herbelin
2000-11-20
[next]