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
*
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
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Possibilité de syntaxe conjointement à la définition des inductifs et des ...
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
coqide: .* on start/add \n on eof
monate
2003-05-14
*
Affichage commentaires
herbelin
2003-05-13
*
Prise en compte des syntaxes v8 dans Uninterpreted Notation
herbelin
2003-04-29
*
Factorisation des produits de même type; parenthèses autour des x:=c et n:=...
herbelin
2003-04-29
*
Moins de ' ' à l'affichage
herbelin
2003-04-29
*
Bug fermeture de stdout
herbelin
2003-04-29
*
Ajout "at next level" dans Notation
herbelin
2003-04-17
*
Ajout option 'Local' à Infix et Notation
herbelin
2003-04-11
*
Suppression de quelques espaces superflus
herbelin
2003-04-10
*
Formattage affichage
herbelin
2003-04-09
*
Correction Show Implicits
herbelin
2003-04-09
*
Mécanisme plus simple et efficace pour traduire les implicites
herbelin
2003-04-09
*
Gestion synchronisation des Impargs.*_out et des Impargs._strict dans Impargs
herbelin
2003-04-09
*
Bugs synchronisation pour gestion traduction des implicites
herbelin
2003-04-09
*
Ajout option -v8 à coqtopnew pour permettre le changement de comportement de...
herbelin
2003-04-09
*
Réorganisation de Impargs + mise en place d'une infrastructure
herbelin
2003-04-09
*
Prise en compte affichage coercions traducteur dans Constrextern
herbelin
2003-04-09
*
Ajout option "Local" à "Open Scope"
herbelin
2003-04-08
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Options d'affichage maintenant dans Constrextern
herbelin
2003-04-07
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
Ajout d'un choix 'onlyparse'
herbelin
2003-03-31
*
Restauration de make_all_different (disparu depuis version 1.74) car sinon de...
herbelin
2003-03-31
*
Implicit Variables Type dans les inductive
herbelin
2003-03-29
*
Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)
herbelin
2003-03-29
*
Ajout de Set Print Width
gregoire
2003-03-26
[next]