index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
Commit message (
Expand
)
Author
Age
*
Traduction PolyList/List dans la qualification
herbelin
2003-12-21
*
Substitution dans REvar et PEvar plutot que encodage via noeud application po...
herbelin
2003-12-19
*
'Eval' protege dans Ppconstrnew; eval n'a pas le meme besoin
herbelin
2003-12-15
*
Nouvelle tactique EExists
clrenard
2003-12-01
*
Renommages discrets dans RIneq et Znumtheory
herbelin
2003-11-29
*
Suite commit precedent
herbelin
2003-11-27
*
Qualification des noms utilisateurs en cas de collision avec un nom nouveau
herbelin
2003-11-27
*
Traduction de @; simplification traduction des ident
herbelin
2003-11-26
*
modif lexer: ident peut commencer par _
barras
2003-11-25
*
Prise en compte des defs syntaxiques dans is_global et global_reference qui p...
herbelin
2003-11-24
*
Traitement plus clair, notamment pour Locate, de quand quoter les composantes...
herbelin
2003-11-22
*
ajout Pnat et Pcompare_antisym
herbelin
2003-11-21
*
Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...
herbelin
2003-11-19
*
reparation bug moins unaire (erreur de PP)
barras
2003-11-18
*
Mise en place systeme de qualification des noms renommes; Renommages dans Rin...
herbelin
2003-11-18
*
New tactics : econstructor, eleft, eright, esplit
clrenard
2003-11-17
*
Un ident filtre est liant seulement si une variable deja liee (sinon bug dans...
herbelin
2003-11-17
*
Bug filtrage pour inversion notation
herbelin
2003-11-16
*
Conflit renommage
herbelin
2003-11-14
*
Oublis dans les rennomages
herbelin
2003-11-14
*
Suppression renommages dans Peano
herbelin
2003-11-14
*
moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...
barras
2003-11-13
*
Nouvelle et derniere vague de renommage
herbelin
2003-11-12
*
Test de la reference principale plutot que le module dans lequel se trouve la...
herbelin
2003-11-12
*
Quelqes renommages lies a Zorder
herbelin
2003-11-09
*
Nouvelle vague de renommage
herbelin
2003-11-05
*
Extension de zarith
herbelin
2003-11-04
*
Extensibilite de la grammaires des patterns
herbelin
2003-11-01
*
Renommage Topconstr.map_aconstr_with_binders_loc
herbelin
2003-11-01
*
Ajout notations pour motifs de Cases; renommage map_aconstr_with_binders_loc
herbelin
2003-11-01
*
Ajout CPatNotation; renommage map_aconstr_with_binders_loc
herbelin
2003-11-01
*
Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...
herbelin
2003-11-01
*
Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...
herbelin
2003-10-30
*
Ajout de Print Visibility
herbelin
2003-10-28
*
Nouveaux renommages; mot-cle 'exists'
herbelin
2003-10-27
*
Nouveaux renommages; Traduction speciale pour 'length nil'
herbelin
2003-10-21
*
Optimisation de gen_constant_in_modules
herbelin
2003-10-21
*
Bug Locate Notation
herbelin
2003-10-21
*
Re-desactivation de l'affichage des projections
herbelin
2003-10-17
*
print_projections a true juste pour le bench nocturne
herbelin
2003-10-16
*
Message d'erreur
herbelin
2003-10-16
*
Debranchement de l'affichage systematique des projections avec la notation po...
herbelin
2003-10-16
*
Debranchement de l'affichage systematique des projections avec la notation po...
herbelin
2003-10-16
*
Gestion encore plus affinee des implicites
herbelin
2003-10-15
*
Gestion affinee des implicites
herbelin
2003-10-14
*
Nouvelles traductions de noms; mot-cle; affichage implicites par le traducteur
herbelin
2003-10-14
*
identityT = identity
herbelin
2003-10-14
*
Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...
herbelin
2003-10-14
*
identity est equivalent sur Type (sauf sans argument)
herbelin
2003-10-10
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
[next]