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
*
Affinement de la gestion des niveaux
herbelin
2002-11-28
*
Correction sur commit précédent
herbelin
2002-11-27
*
Oubli
herbelin
2002-11-26
*
Réaffichage des Syntactic Definition (printer constr_expr).
herbelin
2002-11-26
*
Retablissement Syntactic Definition
herbelin
2002-11-25
*
MAJ delimiters et niveaux d'associativite
herbelin
2002-11-25
*
Z dans les patterns via les scopes
herbelin
2002-11-25
*
Retour sur le choix des delimiteurs
herbelin
2002-11-25
*
Rétablissement printer via ast
herbelin
2002-11-24
*
Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...
herbelin
2002-11-24
*
Installation des printers de nombres pour constr_expr
herbelin
2002-11-24
*
Les parenthèses de la notation '(n)' maintemant mises par ML pour un meilleu...
herbelin
2002-11-20
*
Introduction d'un constructeur ARROW; rétablissement priorités des
herbelin
2002-11-20
*
Problème avec le choix d'introduire une indirection vers un rawconstr pour
herbelin
2002-11-17
*
Passage à une représentation des fixpoints plus primitive dans constr_expr ...
herbelin
2002-11-15
*
Bug factorisation grammaire
herbelin
2002-11-15
*
Compatibilité avec les << >> dans la très ancienne syntaxe des actions
herbelin
2002-11-14
*
Bug factorisation
herbelin
2002-11-14
*
Restauration échappement ML
herbelin
2002-11-14
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' co...
herbelin
2002-11-07
*
fix forbidden currified constructors
ddr
2002-11-07
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Ajout delimiteurs dans les motifs de Cases
herbelin
2002-11-03
*
Désagglutination du squelette de la notation et de sa précédence
herbelin
2002-10-30
*
Mais laisser la syntaxe (!id) aussi disponible !
herbelin
2002-10-29
*
Parenthèse non obligatoires autour de !id sans argument
herbelin
2002-10-29
*
Des critères plus fins d'analyse des implicites automatiques; meilleur affic...
herbelin
2002-10-28
*
Clarification changements autour de Remark/Fact/Local
herbelin
2002-10-23
*
Le test de redondance d'une règle était trop fort
herbelin
2002-10-23
*
Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...
herbelin
2002-10-22
*
Ajout d'un suffixe "as [ names ]" pour nommer manuellement les
herbelin
2002-10-21
*
NewDestruct/NewInduction acceptent l'option "using"
herbelin
2002-10-21
*
Prise en compte des délimiteurs dans les motifs de Cases
herbelin
2002-10-21
*
Prise en compte des délimiteurs dans les motifs de Cases
herbelin
2002-10-21
*
L'application de ltac attend une référence; meilleure protection contre
herbelin
2002-10-14
*
Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une
herbelin
2002-10-14
*
Première proposition d'un type ML exprimant la syntaxe de constr; nettoyage
herbelin
2002-10-13
*
Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...
herbelin
2002-10-13
*
réparation de la protection contre les clauses indiscernables de TACTIC EXTE...
herbelin
2002-10-12
*
Notation 2:Check et 2:Eval
herbelin
2002-10-12
*
Restriction sur la forme des Syntactic Definition et re-localisation en fonct...
herbelin
2002-10-12
*
Lazy manuelles dans le code
coq
2002-10-07
*
Lazy experimentale temporaire...
coq
2002-10-05
*
pretty s'appellait prettyp mais il est revenu sous son ancien nom
herbelin
2002-10-05
*
passage a ocaml 3.06
herbelin
2002-09-27
*
Un peu (plus) d'ordre dans Nametab...
coq
2002-09-24
*
La notation with dependante + affichage dependante de moduels corrige
coq
2002-09-20
*
La notation 'with'. L'interpretation - version preliminaire
coq
2002-08-19
*
Pretty-printing preliminaire des modules, commandes
coq
2002-08-19
[next]