index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
g_constr.ml4
Commit message (
Expand
)
Author
Age
*
- Correction bug dans syntaxe des match (liste de motifs vide était acceptée)
herbelin
2007-08-22
*
Generalized CAMLP4USE for pp dependencies
corbinea
2007-07-16
*
Slight cleanup of refl_omega.ml : in particular it uses now list
letouzey
2007-07-11
*
Prise en compte réversibilité des notations de la forme "Notation Nil := @n...
herbelin
2007-05-10
*
Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y a
herbelin
2007-04-11
*
Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5
herbelin
2007-04-10
*
Extension to the general sequence operator (tactical). Now in addition to ...
emakarov
2007-04-02
*
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-03-19
*
Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.
msozeau
2007-02-16
*
Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
herbelin
2007-02-13
*
Abbreviation of order notation.
msozeau
2007-02-01
*
Fix order of wf and measure arguments, patch Program doc.
msozeau
2007-01-31
*
Remplacement de la dépendance de G_vernac en G_constr (source
herbelin
2006-12-03
*
Notations:
herbelin
2006-10-09
*
- Ajout d'un cast vm dans la syntaxe : x <: t
bgregoir
2006-07-22
*
Correction incohérence parsing de %delim dans les motifs
herbelin
2006-07-12
*
Que le niveau 100 soit associatif à droite dans operconst et à gauche dans ...
herbelin
2006-07-04
*
Extension des motifs disjonctifs au cas de disjonction de motifs multiples
herbelin
2006-07-03
*
Added {measure x f} as a valid recursion order.
msozeau
2006-06-22
*
The "clean integration of subtac" patch.
msozeau
2006-05-29
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Si un fixpoint a plusieurs arguments, mais un seul de type inductif,
letouzey
2006-04-14
*
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
msozeau
2006-03-13
*
Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...
herbelin
2005-12-30
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
Changement des named_context
gregoire
2005-12-02
*
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...
herbelin
2004-12-24
*
Déclaration de '..' comme mot-clé (résoud bug #856)
herbelin
2004-11-17
*
Nouvelle en-tête
herbelin
2004-07-16
*
Parsing des V8Notation avec motif recursif en v7
herbelin
2004-03-17
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Keep structure information for Fixpoint declaration and Fix terms
bertot
2004-02-26
*
Compatibilite %T
herbelin
2003-11-14
*
Compatibilite V7.4 pour le delimiteur de positive
herbelin
2003-11-03
*
Delimiters N devient 'nat'
herbelin
2003-10-10
*
traducteur: affiche les commentaires a l'interieur des commandes
barras
2003-09-22
*
Mise en place d'implicites par noms en v8
herbelin
2003-09-21
*
Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...
herbelin
2003-09-12
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
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
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Affinement nommage des productions
herbelin
2003-03-27
*
*** empty log message ***
barras
2003-03-12
*
Affinement entree annot
herbelin
2003-02-17
*
Adds a possibility to construct a term as if it had been parsed through
bertot
2003-01-30
*
Plus de notation cablees dans 'annot'
herbelin
2002-12-21
*
Meilleure factorisation des entrées NEXT internes
herbelin
2002-12-15
*
Associativité de constr9 et lconst à RIGHTA qui est le plus courant
herbelin
2002-12-02
*
constr9 et lconstr NONA pour une meilleur extensibilité
herbelin
2002-11-29
[next]