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
*
Ajout entree pour exporter les commentaires en mode -xml
herbelin
2004-03-26
*
Code mort
herbelin
2004-03-25
*
Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...
herbelin
2004-03-17
*
Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...
herbelin
2004-03-17
*
Parsing des V8Notation avec motif recursif en v7
herbelin
2004-03-17
*
Utilisation de '..' pour la notation concrete des motifs recursifs de filtrage
herbelin
2004-03-17
*
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
*
Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...
herbelin
2004-03-02
*
Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...
herbelin
2004-03-02
*
Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...
herbelin
2004-03-02
*
Correction oubli du cas pas d'arguments implicites du tout
herbelin
2004-03-02
*
Généralisation du type ltac Identifier en IntroPattern; prise en compte des...
herbelin
2004-03-01
*
Expansion du type par nécessité dans le cas d'affichage d'implicites
herbelin
2004-02-28
*
Keep structure information for Fixpoint declaration and Fix terms
bertot
2004-02-26
*
Correction oubli de report d'une modification de g_vernac (1.69) vers g_verna...
herbelin
2004-02-21
*
- fixed the Assert_failure error in kernel/modops
barras
2004-02-18
*
Ajout de lconstr, constr et binder_constr dans Print Grammar constr
herbelin
2004-02-17
*
export the general function for getting information from the environment
bertot
2004-02-16
*
Uniformisation du comportement de Notation et Reserved Notation
herbelin
2004-02-13
*
Localisation des erreurs d'internalisation des notations de tactiques
herbelin
2004-02-12
*
Suppression de 'Print.' en v8
herbelin
2004-01-29
*
Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...
herbelin
2004-01-29
*
Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ...
herbelin
2004-01-27
*
reparation de qqs bugs du traducteur
barras
2004-01-26
*
Protection table des locations lors de Load (pour coqdoc)
herbelin
2004-01-22
*
Export information des references et location de notations pour coqdoc
herbelin
2004-01-21
*
Le traducteur utilisait un afficheur des reels obsolete et bugge
herbelin
2004-01-20
*
Suppression 'Implicit Arguments On/Off' qui n'a plus lieu d'etre en v8
herbelin
2004-01-20
*
make libraries, lexing of more utf8 symbols
marche
2004-01-14
*
Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...
herbelin
2004-01-13
*
Reference obsolete au niveau 200 de pattern
herbelin
2004-01-13
*
bugs avec Pose et Assert
barras
2004-01-09
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
Bug affichage Decompose
herbelin
2003-12-24
*
*** empty log message ***
barras
2003-12-23
*
Mise en valeur intropattern de paires et acceptation dans le 'as' de inductio...
herbelin
2003-12-22
*
Substitution dans REvar et PEvar plutot que encodage via noeud application po...
herbelin
2003-12-19
*
name_app accessible a tous dans Nameops
herbelin
2003-12-19
*
ajout test de non-regression Clear d'une def locale
barras
2003-12-17
*
MAJ suppression 250
herbelin
2003-12-16
*
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
barras
2003-12-15
*
correction bug: parentheses ne cassent plus les implicites
barras
2003-12-08
*
Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...
herbelin
2003-12-04
*
Symetrisation parsing/printing 'abstract'
herbelin
2003-12-04
*
Nouvelle tactique EExists
clrenard
2003-12-01
*
Ajout ne_string
herbelin
2003-11-27
*
Protection contre les notations vides
herbelin
2003-11-26
*
Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ...
herbelin
2003-11-26
[next]