index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
pr_vernac est paresseux; States.unfreeze seulement après que msgnl ait
herbelin
2003-10-03
*
Correction bug explosion de la taille de la liste loaded_modules
herbelin
2003-10-03
*
Implantation de l'option 'format' des Notations
herbelin
2003-10-01
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Ajout 'About'
herbelin
2003-09-26
*
Decouplage printing en v8 pour les interpretations de notations
herbelin
2003-09-26
*
V8Infix declarait a tort une regle d'interpretation V7
herbelin
2003-09-25
*
Traduction aussi si -translate et -load-vernac-source
herbelin
2003-09-24
*
Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...
herbelin
2003-09-23
*
Utilisation de noms dans 'Implicit Arguments [...]'
herbelin
2003-09-23
*
traducteur: affiche les commentaires a l'interieur des commandes
barras
2003-09-22
*
Anglais
herbelin
2003-09-22
*
message d'erreur de garde des cofix
barras
2003-09-22
*
Renommage Implicits -> Implicit
herbelin
2003-09-21
*
Changement de la politique de V8only: V8only tout seul signifie
herbelin
2003-09-21
*
parsing
herbelin
2003-09-19
*
Plutôt que de faire "Load" silencieusement, en profiter pour traduire
herbelin
2003-09-18
*
Ajout r gle d'affichage tactiques èéfinies par Notation
herbelin
2003-09-18
*
Pour cacher le contenu de Load au traducteur
herbelin
2003-09-16
*
Tentative amelioration pretty-printing symboles
herbelin
2003-09-16
*
(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)...
herbelin
2003-09-16
*
(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)
herbelin
2003-09-16
*
Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...
herbelin
2003-09-12
*
Déplacement d'un morceau de Declare
herbelin
2003-09-12
*
Ajout 'Print Scopes' et 'Bind Scope with classes'
herbelin
2003-09-12
*
Déplacement de Declare et déclarations des scopes d'argument dans Declare
herbelin
2003-09-12
*
Debranchement du traducteur pour Load !
herbelin
2003-09-10
*
Traduction de Distfix
herbelin
2003-09-10
*
Mise en place possibilité de définitions locales dans les paramètres des r...
herbelin
2003-09-06
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
Mise en place possibilité de définitions locales dans les paramètres des i...
herbelin
2003-09-06
*
Freeze mal place
herbelin
2003-09-02
*
Mise en oeuvre de la syntaxe des inductifs a la ML 'Inductive nat : Set := O ...
herbelin
2003-08-31
*
Fusion -translate et -ftranslate
herbelin
2003-08-14
*
Bug et amliorations diverses
herbelin
2003-08-12
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Option -v8 à coqtop lance coqtopnew; option -no-strict; option -no-proofs
herbelin
2003-08-11
*
Nettoyage
herbelin
2003-08-11
*
Bug globalisation Grammar (suite)
herbelin
2003-07-24
*
Bug globalisation
herbelin
2003-07-23
*
Ajout systématique de Proof dans la traduction
herbelin
2003-06-23
*
Ajout option Local à Hint, Hints et HintDestruct
herbelin
2003-06-14
*
Distinction mode v7 ou translate; conséquences du déplacement traducteur de...
herbelin
2003-06-10
*
Déplacement de code dans command; MAJ DebugOn
herbelin
2003-06-10
*
Mise en place structure pour des 'arguments scope' dirigés par une classe
herbelin
2003-06-10
*
Tables logarithmiques pour les coercions + nettoyage
herbelin
2003-06-08
*
fabrication de ide/utf8.vo
letouzey
2003-05-23
*
Bug en mode translate
herbelin
2003-05-23
*
Ajout V8Notation
herbelin
2003-05-22
[next]