index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
egrammar.ml
Commit message (
Expand
)
Author
Age
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
- Cleaning (unification of ML names, removal of obsolete code,
herbelin
2009-04-27
*
- Structuring Numbers and fixing Setoid in stdlib's doc.
herbelin
2009-01-19
*
Affichage des notations récursives:
herbelin
2008-10-22
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Correction d'un autre bug autour de la gestion des niveaux vides de
herbelin
2008-07-11
*
Résolution bug #1850 sur notations avec niveaux inconnus de
herbelin
2008-05-26
*
Contournement laborieux de la "feature" de camlp5 qui entrainait le
herbelin
2008-04-30
*
Bugs, nettoyage, et améliorations diverses
herbelin
2008-04-13
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
gestion speciale du niveau 5 des ltac
barras
2006-11-02
*
Compatibilité hyp=var dans Tactic Notation + nettoyage
herbelin
2006-09-15
*
Changement du type d'argument 'TacticArgType X' en un type
herbelin
2006-06-08
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...
herbelin
2005-12-30
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Simplifification de vernac_expr li l'abandon du traducteur
herbelin
2005-12-23
*
Changement des named_context
gregoire
2005-12-02
*
Affinements suite à extension Tactic Notation aux tacticielles
herbelin
2005-05-17
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
Globalisation des Tactic Notation
herbelin
2005-05-15
*
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...
herbelin
2005-01-02
*
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...
herbelin
2004-12-25
*
Correction bug Notation: il faut re-déclarer les règles de parsing des nota...
herbelin
2004-11-22
*
Nouvelle en-tête
herbelin
2004-07-16
*
Mise en place de motifs récursifs dans Notation; quelques simplifications au...
herbelin
2004-03-17
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'
herbelin
2004-03-03
*
Keep structure information for Fixpoint declaration and Fix terms
bertot
2004-02-26
*
- fixed the Assert_failure error in kernel/modops
barras
2004-02-18
*
Localisation des erreurs d'internalisation des notations de tactiques
herbelin
2004-02-12
*
reparation de qqs bugs du traducteur
barras
2004-01-26
*
name_app accessible a tous dans Nameops
herbelin
2003-12-19
*
Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons...
herbelin
2003-11-20
*
Protection contre l'effacement des niveaux vides de operconstr et pattern par...
herbelin
2003-11-19
*
Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammar
herbelin
2003-11-15
*
En v8, une notation, c'est 2 regles et un niveau
herbelin
2003-11-04
*
Extensibilite de la grammaires des patterns
herbelin
2003-11-01
*
On n'autorise plus les niveaux doubles L/R en v8
herbelin
2003-10-17
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Passage des projections au niveau 1
herbelin
2003-09-10
*
9 est associatif a gauche
herbelin
2003-09-10
*
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-09-09
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Localisation erreurs TacAlias; Globalisation moins tolérante dans les
herbelin
2003-04-28
*
simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...
letouzey
2003-04-16
*
*** empty log message ***
barras
2003-03-12
*
Prise en compte notations dans les extensions de motiff
herbelin
2002-12-28
[next]