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
*
Prise en compte du repertoire dans le section path; utilisation de dirpath po...
herbelin
2000-11-28
*
Ajout des Fix et CoFix dans les patterns
delahaye
2000-11-28
*
Elimination du '
delahaye
2000-11-28
*
Bug affichage inductifs
herbelin
2000-11-27
*
uniformisation messages d'erreur
filliatr
2000-11-27
*
Prise en compte des implicites de locaux à l'affichage
herbelin
2000-11-27
*
Affichage des définitions locales
herbelin
2000-11-27
*
Restruration autour de qualidarg
herbelin
2000-11-26
*
Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...
herbelin
2000-11-26
*
Prise en compte noms longs dans divers fonctions de Print
herbelin
2000-11-26
*
Réorganisation autour de globalize_constr
herbelin
2000-11-24
*
Nettoyage
herbelin
2000-11-24
*
Ajout d'un .:/opt/kde/bin:/home/herbelin/bin:/bin:/sbin:/usr/bin:/usr/etc:/us...
herbelin
2000-11-24
*
Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab
filliatr
2000-11-24
*
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
[next]