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
*
Fusion des g_*syntaxnew.ml avec les g_*syntax.ml avec sélection dynamique selon
herbelin
2003-09-12
*
Ajout 'Print Scopes' et 'Bind Scope with classes'
herbelin
2003-09-12
*
MAJ module requis pour le parsing des numéraux
herbelin
2003-09-12
*
Affichage des scopes d'arguments
herbelin
2003-09-12
*
Ajout 'Print Scopes' et 'Bind Scope with classes'; 'Delimits' -> 'Delimit'
herbelin
2003-09-12
*
Passage des projections au niveau 1
herbelin
2003-09-10
*
9 est associatif a gauche
herbelin
2003-09-10
*
Traduction de Distfix
herbelin
2003-09-10
*
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
[next]