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
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
petit bug -byte/-opt (execv -> execvp) et message coercion teste is_silent
filliatr
2000-12-12
*
Ajout erreur DoesNotOccurIn
herbelin
2000-12-06
*
Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard...
herbelin
2000-12-06
*
Reparation conditions de positivites inductifs, echange dans add_entry
mohring
2000-12-06
*
Mini-nettoyage noms longs
herbelin
2000-12-05
*
caractere opaque des constantes repris en compte
filliatr
2000-12-04
*
Changement de la syntaxe des options -I et -R
herbelin
2000-11-30
*
Bug option -I et -R quand le répertoire est '..'
herbelin
2000-11-29
*
Bug option -I et -R quand le répertoire est '.'
herbelin
2000-11-29
*
Suppression cast inutile
herbelin
2000-11-29
*
Now AddRecPath and AddPath can be used with an As option to specify the
sacerdot
2000-11-29
*
load_path_entry structure simplified; field relative_subdir renamed to coq_di...
sacerdot
2000-11-29
*
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
[next]