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
*
Parsing au niveau lconstr des patterns de 'match context'
herbelin
2003-09-21
*
Changement de la politique de V8only: V8only tout seul signifie
herbelin
2003-09-21
*
Mise en place d'implicites par noms en v8
herbelin
2003-09-21
*
Conflit de nom Pplus dans positive et dans polynomial (de ring)
herbelin
2003-09-21
*
Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...
herbelin
2003-09-21
*
Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...
herbelin
2003-09-21
*
Nettoyage
herbelin
2003-09-21
*
coqide auto complete initial bug fix
marche
2003-09-19
*
Coqide : les nouveaute d'aout
monate
2003-09-19
*
'::' est deja pris en V7
herbelin
2003-09-19
*
maj
filliatr
2003-09-19
*
Section et report Infix hors section
herbelin
2003-09-19
*
Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr...
herbelin
2003-09-19
*
Mise en place des V8Notation et V8Infix pour déclarer des notations en
herbelin
2003-09-19
*
Ajout notation :: pour cons
herbelin
2003-09-19
*
Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...
herbelin
2003-09-19
*
parsing
herbelin
2003-09-19
*
Interface Eauto
herbelin
2003-09-18
*
Traduction de Instantiate
herbelin
2003-09-18
*
Niveau du 'as' des motifs
herbelin
2003-09-18
*
Traduction de '_' comme reference
herbelin
2003-09-18
*
Parsing correct des explicites en cas de projection
herbelin
2003-09-18
*
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
*
Simplification afficheur de tactiques non primitive
herbelin
2003-09-18
*
bug fix: term reduced in bad env
barras
2003-09-18
*
maj
filliatr
2003-09-17
*
En attendant l'afficheur...
herbelin
2003-09-16
*
Pour appliquer les noms reserves aussi aux binders
herbelin
2003-09-16
*
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
*
Reprise de coqbinaries dans translation
herbelin
2003-09-15
*
Bug PR#324
herbelin
2003-09-14
*
Indirection pour coqlib8 pour que la cible newtheories/%.v soit choisie
herbelin
2003-09-13
*
Deplacement de Declare vers Termops
herbelin
2003-09-13
*
maj
filliatr
2003-09-13
*
Retour à des cibles plus explicites: world7 et world8, install7 et install8
herbelin
2003-09-12
*
Outil de test de la traduction et de la compilation en v8 sans modification des
herbelin
2003-09-12
*
Ajout install7 et coqwc dans tools
herbelin
2003-09-12
*
Ajout cible world7
herbelin
2003-09-12
*
Divers
herbelin
2003-09-12
*
Ajout nouvelles commandes
herbelin
2003-09-12
*
Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...
herbelin
2003-09-12
*
Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...
herbelin
2003-09-12
*
Suppression DatatypesSyntax et PeanoSyntax qui était vides
herbelin
2003-09-12
*
Fusion des g_*syntaxnew.ml avec les g_*syntax.ml avec sélection dynamique selon
herbelin
2003-09-12
*
Inclusion automatique de highparsing
herbelin
2003-09-12
*
Suppression DatatypesSyntax et PeanoSyntax qui était vides
herbelin
2003-09-12
[next]