index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
Un axiome en attendant la mise a jour de la preuve de times_convert
herbelin
2002-12-06
*
Amélioration sensible de l'efficacité de Zmult et times
herbelin
2002-12-06
*
Amélioration sensible de l'efficacité de la multiplication
herbelin
2002-12-06
*
maj
filliatr
2002-12-06
*
Ajout affichage fconstr
herbelin
2002-12-05
*
reorganisation des recherches de ref dans ml_decl
letouzey
2002-12-05
*
code cleanup (+ debut de commencement de modules)
letouzey
2002-12-05
*
des Set et des Map en plus
letouzey
2002-12-05
*
Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...
herbelin
2002-12-04
*
Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...
herbelin
2002-12-04
*
Modification Require From
mohring
2002-12-04
*
Correction d'un message d'erreur de l'application de non-foncteur
coq
2002-12-04
*
mdule --> module
mohring
2002-12-04
*
suppression du champ mind_singl inutilisé dans mutual_inductive_body
letouzey
2002-12-04
*
Corrige un bug de composition de substitutions
coq
2002-12-04
*
fichiers DOS
filliatr
2002-12-04
*
maj
filliatr
2002-12-04
*
la table PARAMETER n'existe plus (mergé dans la table CONSTANT)
letouzey
2002-12-03
*
MAJ travail moulinette
herbelin
2002-12-03
*
bug de non-indépendance des règles d'affichage et parsing vis à vis du nom...
herbelin
2002-12-03
*
bugs d'affichage (confusion key/scope dans les délimiteurs)
herbelin
2002-12-03
*
Préparation à la prise en compte des changements de scopes internes aux not...
herbelin
2002-12-03
*
MAJ
herbelin
2002-12-03
*
Essai d'introduction d'un scope des types
herbelin
2002-12-03
*
Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvelles
bertot
2002-12-03
*
Pas de globalisation impérative pour les Grammar
herbelin
2002-12-03
*
Calcul de l'associativité même pour les Grammar avec plusieurs clauses
herbelin
2002-12-03
*
Le '.' peut faire partie d'un token
herbelin
2002-12-03
*
maj
filliatr
2002-12-03
*
Remplacement Grammar par Notation
herbelin
2002-12-02
*
MAJ sur MAJ
herbelin
2002-12-02
*
Remplacement de Syntactic Definition par Notation
herbelin
2002-12-02
*
Associativité de constr9 et lconst à RIGHTA qui est le plus courant
herbelin
2002-12-02
*
Ajout des options "Set Contextual Implicits" et "Set Strict Implicits
herbelin
2002-12-02
*
Re-déplacement du résultat de Grammar au niveau constr_expr (globalisation ...
herbelin
2002-12-02
*
Ajout des options "Set Contextual Implicits" et "Set Strict Implicits
herbelin
2002-12-02
*
Re-déplacement du résultat de Grammar au niveau constr_expr
herbelin
2002-12-02
*
Z_scope doit annuler l'affichage de = entre
herbelin
2002-12-02
*
On force l'associativité pour les entrées sans niveaux
herbelin
2002-12-02
*
Synchro level (suite)
herbelin
2002-12-01
*
maj
filliatr
2002-11-30
*
2 bugs: 1) projections pas renommées 2) mutual fixpoints a l'envers
letouzey
2002-11-29
*
Raffinement syntaxe Infix
herbelin
2002-11-29
*
Utilisation de Snext pour gérer les symboles non associatifs
herbelin
2002-11-29
*
MAJ
herbelin
2002-11-29
*
Synchro de la table des niveaux avec les sections
herbelin
2002-11-29
*
constr9 et lconstr NONA pour une meilleur extensibilité
herbelin
2002-11-29
*
Re-échappement des \ et " dans les token string
herbelin
2002-11-29
*
maj
filliatr
2002-11-29
*
cosmetique
letouzey
2002-11-29
[prev]
[next]