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
*
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-09-09
*
'Grammar tactic' devient 'Tactic Notation'
herbelin
2003-09-09
*
Traduction des réferences arguments de commandes non primitives
herbelin
2003-09-09
*
Code mort
herbelin
2003-09-09
*
Mise en place possibilité de définitions locales dans les paramètres des r...
herbelin
2003-09-06
*
Mise en place possibilité de définitions locales dans les paramètres des r...
herbelin
2003-09-06
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
'Implicits qid' -> 'Implicit Arguments qid'
herbelin
2003-09-06
*
Adapter l'entree de grammaire a la version 7 ou 8
herbelin
2003-09-06
*
Mise en place possibilité de définitions locales dans les paramètres des i...
herbelin
2003-09-06
*
Passage de lconstr à constr pour les arguments immédiat de commandes
herbelin
2003-09-06
*
Passage de lconstr à constr pour les arguments immédiat de commandes
herbelin
2003-09-06
*
Bug affichage tactiques supplementaires en v8 (suite)
herbelin
2003-09-06
*
Bug affichage tactiques supplementaires en v8
herbelin
2003-09-05
*
Impression sans ',' des constructeurs de meme type, pour v8
herbelin
2003-09-05
*
Relachement conflit 'with' dans le cas des Module with Definition
herbelin
2003-09-02
*
'Assumptions' sur le modèle général des lieurs
herbelin
2003-08-31
*
Affichage des inductifs en v8
herbelin
2003-08-31
*
Pb de mot-cle
herbelin
2003-08-14
*
Ajout token '!' pour correctness
herbelin
2003-08-14
*
Enregistrement tuple_constr
herbelin
2003-08-14
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Bug compilation
herbelin
2003-06-20
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'
herbelin
2003-06-19
*
Ajout option Local aux Hint
herbelin
2003-06-17
*
Ajout option Local à Hint, Hints et HintDestruct
herbelin
2003-06-14
*
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
[next]