index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
syntax
Commit message (
Expand
)
Author
Age
*
Nouvelle en-tête
herbelin
2004-07-16
*
Preservation affichage des ?n en V7
herbelin
2003-05-22
*
Affichage META
herbelin
2003-05-19
*
Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...
herbelin
2003-04-27
*
notations <>, Assumption avec existentiel, replace term
mohring
2003-03-28
*
Ajout de Set Print Width
gregoire
2003-03-26
*
Bugs affichage
herbelin
2003-01-16
*
Introduction d'un constructeur ARROW; rétablissement priorités des
herbelin
2002-11-20
*
Correction des priorités des TOMATCH
herbelin
2002-11-20
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Des critères plus fins d'analyse des implicites automatiques; meilleur affic...
herbelin
2002-10-28
*
Bug qui empêchait "0" d'être parenthèsé
herbelin
2002-10-21
*
Parenthèses forcées autour des arguments d'une application pour parser
herbelin
2002-10-14
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
syntax/PPTactic.v passe au niveau ML
herbelin
2002-05-29
*
Ajout EVAL
herbelin
2002-05-29
*
Ajout de Eval, Inst et Check
delahaye
2002-05-27
*
bad printing of Zeta reduction flags (was missing)
barras
2002-02-11
*
Ajout tactiques Rename et Pose; modifications pour Inversion
herbelin
2002-02-01
*
Affichage NewInduction/NewDesctruct
herbelin
2001-12-13
*
Affichage des '_' pour Intros
herbelin
2001-12-06
*
Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]b
herbelin
2001-11-08
*
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
*
Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...
herbelin
2001-10-05
*
Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction
herbelin
2001-08-05
*
Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...
herbelin
2001-06-25
*
Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Case
clrenard
2001-06-11
*
Facilites pour le debogguage des univers.
coq
2001-05-29
*
Reorganisation pour Ltac
delahaye
2001-04-24
*
Ajout de syntaxe pour Ltac
delahaye
2001-04-23
*
Reparation de l'affichage des THEN's
delahaye
2001-04-13
*
Bug affichage LETPATTERN
herbelin
2001-04-10
*
Interprétation des qualidarg
herbelin
2001-03-27
*
Les règles d'affichage ajoutés dans le commit précédent avait le même no...
herbelin
2001-03-23
*
Règle de syntaxe pour CASTEDCOMMAND
herbelin
2001-03-22
*
entetes
filliatr
2001-03-15
*
Ajout du Match Context
delahaye
2001-02-07
*
Affichage des QUALID
herbelin
2000-11-23
*
Traitement du pretty-print des Redexp
delahaye
2000-11-21
*
Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...
herbelin
2000-10-18
*
Niveau d'associativité du let
herbelin
2000-10-11
*
Code mort (2ème)
herbelin
2000-10-05
*
Code mort
herbelin
2000-10-05
*
Renommage tactique Let en LetTac
herbelin
2000-10-03
*
Bugs parenthèses
herbelin
2000-09-14
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Réparation bug d'affichage et affichage des instanciations par des {...}
herbelin
2000-05-23
*
Déplacement du type reference dans Term
herbelin
2000-04-28
*
Affichage des <> pour débug
herbelin
2000-03-20
*
Bugs
herbelin
2000-01-11
[next]