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
*
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
*
Ajout de Record
herbelin
2000-01-11
*
Déplacement non-affichage des coercions dans termast
herbelin
2000-01-07
*
Nouveaux types 'constructor' et 'inductive' dans Term;
herbelin
1999-12-15
*
- constantes avec recettes
filliatr
1999-12-09
*
deplacement de Discharge dans toplevel
filliatr
1999-12-08
*
premier debugage
filliatr
1999-12-05
*
- global_reference traite des variables
filliatr
1999-12-03
*
Version initiale
herbelin
1999-12-02