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
*
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
*
Pb residuel avec la prise en compte des parametres implicites d'inductifs
herbelin
2003-10-08
*
Prise en compte des paramètres implicites d'inductifs pour la globalisation ...
herbelin
2003-10-08
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
cosmetique
herbelin
2003-10-01
*
Les notations hors scope s'empilent maintenant comme des scopes ne
herbelin
2003-09-30
*
code mort
herbelin
2003-09-30
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Prise en compte d'un inductif sans argument dans le 'in' des 'match'
herbelin
2003-09-29
*
Syntaxe plus liberale pour le type des arguments de filtrage du 'match'
herbelin
2003-09-26
*
Syntaxe plus liberale pour le type des arguments de filtrage du 'match'; trad...
herbelin
2003-09-26
*
Nouvelle serie de traductions
herbelin
2003-09-26
*
Un peu plus de souplesse dans la globalisation des noms utilises par les tact...
herbelin
2003-09-26
*
Decouplage printing en v8 pour les interpretations de notations
herbelin
2003-09-26
*
Changement de l'afficheur pour que les variables liées aient un nom indépen...
herbelin
2003-09-23
*
traducteur: affiche les commentaires a l'interieur des commandes
barras
2003-09-22
*
Bug d'externalisation des constantes avec uniquement des implicites
herbelin
2003-09-22
*
Mise en place d'implicites par noms en v8
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
*
parsing
herbelin
2003-09-19
*
Traduction de '_' comme reference
herbelin
2003-09-18
*
Parsing correct des explicites en cas de projection
herbelin
2003-09-18
*
Activation déclaration automatique de scope d'arguments; affichage scopes d'...
herbelin
2003-09-12
*
Activation déclaration automatique de scope d'arguments
herbelin
2003-09-12
*
Scope type pour le codomaine de Prod aussi; ajout extern_rawtype
herbelin
2003-09-12
*
Scope type pour le codomaine de Prod aussi
herbelin
2003-09-12
*
open superflu
herbelin
2003-09-12
*
Renommage des variables '_'
herbelin
2003-09-10
[next]