index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
command.ml
Commit message (
Expand
)
Author
Age
...
*
Petit netoyage dans lib
coq
2002-12-19
*
Prise en compte des scopes traversés dans les notations
herbelin
2002-12-15
*
Code mort ?
herbelin
2002-12-09
*
Réaffichage des Syntactic Definition (printer constr_expr).
herbelin
2002-11-26
*
Passage à une représentation des fixpoints plus primitive dans constr_expr ...
herbelin
2002-11-15
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Un Local construit par preuve hors section doit être considéré global
herbelin
2002-11-06
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Clarification changements autour de Remark/Fact/Local
herbelin
2002-10-23
*
Que des niveaux d'univers frais dans le type des constantes globales
herbelin
2002-09-29
*
Que des niveaux d'univers frais dans le type des constantes globales
herbelin
2002-09-29
*
Suppression automatique du corps des définitions locales opaques dans
herbelin
2002-08-17
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour
herbelin
2002-07-11
*
Intgration uniforme de coercions dans les dclarations (Variable and co) et re...
herbelin
2002-06-03
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
compat ocaml 3.03
filliatr
2001-12-13
*
Prise en compte des '?' aussi dans le type des définitions
herbelin
2001-11-21
*
Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant
herbelin
2001-11-20
*
Mise en place d'une méthode directe pour indiquer le type des déclarations ...
herbelin
2001-11-19
*
GROS COMMIT:
barras
2001-11-05
*
Vérification précoce qu'un lemme n'existe pas déjà
herbelin
2001-10-26
*
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
*
Transformation de Remark/Fact en constantes non visibles sans qualification
herbelin
2001-09-14
*
Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...
herbelin
2001-09-10
*
Parsing
herbelin
2001-08-10
*
anomaly -> error
clrenard
2001-07-10
*
Changement de la structure des points fixes
barras
2001-05-03
*
un typage sûr pour Goal et Check
filliatr
2001-04-20
*
Interdiction des 'Save (thm_tok)? id' si thm pas ouvert par Goal
herbelin
2001-04-09
*
Uniformisation des 'Save def_tok id'
herbelin
2001-04-09
*
utilisation de Options.if_verbose
filliatr
2001-04-03
*
entetes
filliatr
2001-03-15
*
Erreur sur commit
herbelin
2001-02-14
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
Ré-introduction des implicites à la volée dans la définition des inductifs
herbelin
2001-01-27
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Réorganisation suite ajout de constantes locales dans les Records
herbelin
2001-01-24
*
Rattrapage d'erreur pour le Case + Eval Compute in pour Definition
delahaye
2001-01-03
*
Ajout du Let pour le langage de tactiques
delahaye
2000-12-29
*
Découpage des différentes fonctionnalités de build_mutual et definition_st...
herbelin
2000-12-19
*
Bug des locaux au premier niveau des modules qui disparaissaient de l'environ...
herbelin
2000-12-15
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
caractere opaque des constantes repris en compte
filliatr
2000-12-04
*
Distinction local/global
herbelin
2000-11-27
[prev]
[next]