index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
Ajout d'une option d'alias à -I
herbelin
2000-11-29
*
Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ch...
herbelin
2000-11-29
*
Remplacement des add_include par add_rec_include pour avoir le repertoire dan...
herbelin
2000-11-28
*
Prise en compte du repertoire dans le section path; utilisation de dirpath po...
herbelin
2000-11-28
*
Distinction local/global
herbelin
2000-11-27
*
uniformisation messages d'erreur
filliatr
2000-11-27
*
Prise en compte des définitions locales
herbelin
2000-11-27
*
Branchement des Local sur des SectionLocalDef
herbelin
2000-11-27
*
Prise en compte noms longs dans divers fonctions de Print
herbelin
2000-11-26
*
Remplacement de certains sp_of_id par des locate
herbelin
2000-11-26
*
sp au lieu de id dans END-SECTION
herbelin
2000-11-26
*
Réorganisation autour de globalize_constr
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
*
- coqc: utilise le meilleur coq possible
filliatr
2000-11-24
*
print_id, print_sp -> pr_id, pr_sp
herbelin
2000-11-23
*
Informations inutiles
herbelin
2000-11-23
*
print_id, print_sp -> pr_id, pr_sp
herbelin
2000-11-23
*
Bug qualidconstarg (intervient pour Transparent)
herbelin
2000-11-23
*
Reparation IsMutConstruct + Transparent
mohring
2000-11-23
*
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...
herbelin
2000-11-22
*
Nettoyage
herbelin
2000-11-22
*
deplacement poly_args; iterateurs sur les segments
filliatr
2000-11-22
*
retablissement de line_oriented_parser pour Yves
filliatr
2000-11-22
*
Elimination d'un test sur les macros
delahaye
2000-11-21
*
implicites manuels
filliatr
2000-11-21
*
Begin-End Silent deviennent Set?Unset Silent
mohring
2000-11-21
*
separation calcul des implicites et declaration des constantes / inductifs / ...
filliatr
2000-11-21
*
Petit bug entre close_section's
herbelin
2000-11-20
*
Prise en compte des noms qualifiés dans certaines commandes
herbelin
2000-11-20
*
Prise en compte noms longs
herbelin
2000-11-20
*
Tables séparées pour chaque type de global; calcul de la Nametab de la sect...
herbelin
2000-11-20
*
Ajout erreur GlobalNotFound
herbelin
2000-11-20
*
Mieux à sa place dans toplevel
herbelin
2000-11-20
*
Prise en compte noms longs
herbelin
2000-11-20
*
Une capsule pour save_module_to dans Discharge
herbelin
2000-11-20
*
methode export
filliatr
2000-11-15
*
Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...
herbelin
2000-11-10
*
Renommage canonique SectionLocalDecl -> SectionLocalAssum
herbelin
2000-11-09
*
nouveau load path
filliatr
2000-11-08
*
amélioration
herbelin
2000-11-08
*
out_variable (Liboject.obj -> ...) distibgue de get_variable
filliatr
2000-11-08
*
Modification de la table des tactic Definitions pour eviter l'ecriture
mohring
2000-11-07
*
Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...
herbelin
2000-11-06
*
print_idl inliné
herbelin
2000-11-06
*
nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...
filliatr
2000-11-06
*
compilation avec make de Solaris; README et INSTALL
filliatr
2000-11-03
*
correction Abstract (et make world passe!)
filliatr
2000-11-02
*
suppression des (* open Generic *)
filliatr
2000-11-02
[next]