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
*
certains effets disparaissent a la sortie des sections, d'autres non (selon S...
filliatr
2000-11-24
*
SearchPattern et SearchRewrite
filliatr
2000-11-24
*
Ajout d'une syntaxe pour Reals.
mayero
2000-11-23
*
Search réparé
filliatr
2000-11-23
*
Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_sp
herbelin
2000-11-23
*
Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;
herbelin
2000-11-23
*
Bug qualidconstarg (intervient pour Transparent)
herbelin
2000-11-23
*
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...
herbelin
2000-11-22
*
deplacement poly_args; iterateurs sur les segments
filliatr
2000-11-22
*
Begin-End Silent deviennent Set?Unset Silent
mohring
2000-11-21
*
Prise en compte des implicites dans les regles de grammaires
herbelin
2000-11-21
*
La variable argument d'un non-terminal dans Grammar est maintenant un Var ( p...
herbelin
2000-11-20
*
Prise en compte des noms qualifiés dans certaines commandes
herbelin
2000-11-20
*
Nouveau lexeme METAIDENT pour les $id
herbelin
2000-11-20
*
Ajout diverses entrées pour les noms qualifiés
herbelin
2000-11-20
*
Prise en compte des noms qualifiés dans certaines commandes
herbelin
2000-11-20
*
Acceptation des noms qualifiés; utilisation de global_reference dans pattern...
herbelin
2000-11-20
*
Nouvelle entrée qualidarg pour noms qualifiés; nouveau lexeme METAIDENT pou...
herbelin
2000-11-20
*
Acceptation des noms qualifiés; nouveau lexeme METAIDENT pour les $id
herbelin
2000-11-20
*
"Distinction entre . suivi d'un blanc et . suivi d'un ident (pour les noms qu...
herbelin
2000-11-20
*
Utilisation de global_reference dans pattern
herbelin
2000-11-20
*
Utilisation de global_reference dans rawconstr
herbelin
2000-11-20
*
Prise en compte constructeur QUALID pour noms qualifiés
herbelin
2000-11-20
*
Prise en compte des noms qualifiés dans certaines commandes; nouveau lexeme ...
herbelin
2000-11-20
*
Ajout pr_global_reference et is_visible
herbelin
2000-11-20
*
Amélioration message d'erreur arg explicité au lieu d'arg normal
herbelin
2000-11-09
*
nouveau load path
filliatr
2000-11-08
*
out_variable (Liboject.obj -> ...) distibgue de get_variable
filliatr
2000-11-08
*
MAJ
herbelin
2000-11-07
*
Changement/extension dans les noms de parseurs de Grammar
herbelin
2000-11-07
*
Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...
herbelin
2000-11-06
*
nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...
filliatr
2000-11-06
*
Nouveau mode de compilation de .ml4
herbelin
2000-11-05
*
Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...
herbelin
2000-11-05
*
compilation des fichiers ml4 sans GNUseries
filliatr
2000-11-03
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
- simplification Makefile (compilation des fichiers .ml'; pas encore parfait
filliatr
2000-10-31
*
Priorite du Try/Orelse + Debug switch + correction bug dans Pattern
delahaye
2000-10-30
*
Renommage var en named et decl en assum
herbelin
2000-10-26
*
Bug de copier-coller
herbelin
2000-10-24
*
Pb affichage warning
herbelin
2000-10-21
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Renommage canonique :
herbelin
2000-10-18
*
Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...
herbelin
2000-10-18
*
2ème
herbelin
2000-10-18
*
Mise en place de parseurs avec globalisation pas seulement dans les quotation...
herbelin
2000-10-18
*
Nettoyage
herbelin
2000-10-18
*
globalize_command devient globalize_constr
herbelin
2000-10-18
*
Correction pb de globalisation dans print_mutual
herbelin
2000-10-18
*
Pb factorisation de Print Grammar
herbelin
2000-10-17
[next]