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
*
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
*
Ajout 'mod' comme keyword
herbelin
2003-09-10
*
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-09-09
*
Ajout If; synchro avec constrextern
herbelin
2003-09-09
*
Ajout If; renommage de l'ident '_'
herbelin
2003-09-09
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
cosmetique
herbelin
2003-09-06
*
Plus de passage du scope tmp sous les lambdas
herbelin
2003-09-02
*
Symetrisation des changements implicites de scope
herbelin
2003-08-31
*
Traducteur de correctness
herbelin
2003-08-14
*
Bug et améliorations diverses
herbelin
2003-08-12
*
Ajout LetTuple
herbelin
2003-08-11
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Déplacement traducteur de nom dans Constrextern pour accès aux noms longs
herbelin
2003-06-10
*
Amélioration afficheur de Cases pour les constr_pattern
herbelin
2003-06-10
*
Extension de Locate sur les symboles avec recherche de sous-chaînes; mise en...
herbelin
2003-06-10
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Restructuration des procédures de filtrage
herbelin
2003-05-19
[next]