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
*
Mise en place possibilité de définitions locales dans les paramètres des i...
herbelin
2003-09-06
*
Mise en oeuvre de la syntaxe des inductifs a la ML 'Inductive nat : Set := O ...
herbelin
2003-08-31
*
Mise en place structure pour des 'arguments scope' dirigés par une classe
herbelin
2003-06-10
*
Possibilité de syntaxe conjointement à la définition des inductifs et des ...
herbelin
2003-05-21
*
Prise en compte des syntaxes v8 dans Uninterpreted Notation
herbelin
2003-04-29
*
Ajout "at next level" dans Notation
herbelin
2003-04-17
*
Ajout option 'Local' à Infix et Notation
herbelin
2003-04-11
*
Réorganisation de Impargs + mise en place d'une infrastructure
herbelin
2003-04-09
*
Ajout d'un choix 'onlyparse'
herbelin
2003-03-31
*
Implicit Variables Type dans les inductive
herbelin
2003-03-29
*
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
[next]