index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
Commit message (
Expand
)
Author
Age
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Token '.(' seulement pour v8, sinon conflit avec '.(*'
herbelin
2003-06-11
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
freshid -> fresh
herbelin
2003-06-10
*
Tables logarithmiques pour les coercions + nettoyage
herbelin
2003-06-08
*
Bug
herbelin
2003-05-26
*
Ajout FreshId
herbelin
2003-05-24
*
Ajout V8Notation
herbelin
2003-05-22
*
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
*
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...
herbelin
2003-05-21
*
Possibilité de syntaxe conjointement à la définition des inductifs et des ...
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Petite correction d'affichage de modules
coq
2003-05-08
*
Prise en compte des syntaxes v8 dans Uninterpreted Notation
herbelin
2003-04-29
*
Prise en compte des syntaxes v8 dans Uninterpreted Notation
herbelin
2003-04-29
*
Factorisation des produits de même type; parenthèses autour des x:=c et n:=...
herbelin
2003-04-29
*
Factorisation des produits de même type; parenthèses autour des x:=c et n:=...
herbelin
2003-04-29
*
Ajout is_ident_tail
herbelin
2003-04-29
*
Localisation erreurs TacAlias; Globalisation moins tolérante dans les
herbelin
2003-04-28
*
Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...
herbelin
2003-04-27
*
Reparation affichage LetTac
herbelin
2003-04-27
*
extension des caracteres UTF 8 autorises dans les symboles
filliatr
2003-04-25
*
Ajout "at next level" dans Notation
herbelin
2003-04-17
*
simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...
letouzey
2003-04-16
*
Localisation des appels de tactiques définies sans arguments
herbelin
2003-04-14
*
Correction bug PR#278
coq
2003-04-14
*
Ajout option 'Local' à Infix et Notation
herbelin
2003-04-11
*
Affichage forcé des implicites contextuels si pas de contexte connu
herbelin
2003-04-10
*
Réorganisation de Impargs + mise en place d'une infrastructure
herbelin
2003-04-09
*
Ajout option "Local" à "Open Scope"
herbelin
2003-04-08
*
lconstr pour genterm en v8
herbelin
2003-04-07
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Ajout cas Match
herbelin
2003-04-07
*
Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun implicite
herbelin
2003-04-07
*
Options d'affichage maintenant dans Constrextern
herbelin
2003-04-07
*
espace manquant
herbelin
2003-04-02
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
Bug pattern_occ_hyp_list
herbelin
2003-03-31
*
Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)
herbelin
2003-03-29
*
notations <>, Assumption avec existentiel, replace term
mohring
2003-03-28
*
MAJ des mots-clés, Definition, Theorem, ...
herbelin
2003-03-27
*
MAJ des mots-clés, Definition, Theorem, ...
herbelin
2003-03-27
*
Affinement nommage des productions
herbelin
2003-03-27
*
*** empty log message ***
barras
2003-03-21
*
reparations suite a la nouvelle syntaxe:
barras
2003-03-14
*
Ajout réaffichage SubClass
herbelin
2003-03-13
*
*** empty log message ***
barras
2003-03-12
*
Renommage indpar pour usage plus general
herbelin
2003-03-12
*
Bug délimiteur de scope en vieil affichage ast
herbelin
2003-03-04
[next]