index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
Commit message (
Expand
)
Author
Age
*
construct_reference regarde d'abord dans le contexte local, puis les globaux
filliatr
2001-05-11
*
quelques bug reports mineurs
barras
2001-05-07
*
Changement de la structure des points fixes
barras
2001-05-03
*
Added a flag that makes it possible to re-load files while taking only the
bertot
2001-04-04
*
utilisation de Options.if_verbose
filliatr
2001-04-03
*
La strategie de recherche de lookup_eliminator etait insuffisante
herbelin
2001-03-23
*
entetes
filliatr
2001-03-15
*
protection contre certaines exceptions levees par marshal_{in,out}
barras
2001-03-09
*
on gele apres un Require => meilleures performances memoire, en particulier p...
filliatr
2001-03-06
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
bug Reset et Sections
filliatr
2001-02-28
*
ident au lieu de string pour le nom de base de qualid
herbelin
2001-02-16
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
prise en compte des défs locales dans les arguments des inductifs; meilleure...
herbelin
2001-02-14
*
simplification du make depend; fonctions de stat. util. memoire dans certains...
filliatr
2001-02-08
*
Meilleure approche du conflit path/freeze/library_root en séquentialisant la...
herbelin
2001-02-07
*
Probleme synchronisation roots / inputstate
herbelin
2001-02-07
*
Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir
herbelin
2001-02-07
*
Message d'erreur absolute_reference
herbelin
2001-02-07
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Meilleur traitement des noms explicites dans la Nametab; Différentation du t...
herbelin
2001-02-05
*
Ajout alias mutual_inductive_path = section_path
herbelin
2001-01-27
*
Ré-introduction des implicites à la volée dans la définition des inductifs
herbelin
2001-01-27
*
Remplacement d'un bug non documente par un autre documente dans quantify_extr...
herbelin
2001-01-25
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Réorganisation suite ajout de constantes locales dans les Records
herbelin
2001-01-24
*
Ajout du Let pour le langage de tactiques
delahaye
2000-12-29
*
find_section_variable : un traducteur id -> sp pour variables de section; var...
herbelin
2000-12-25
*
Test pour empêcher 2 sections de même noms
herbelin
2000-12-20
*
Import module force l'ouverture du module même s'il était déjà ouvert afi...
herbelin
2000-12-20
*
Pédagogie
herbelin
2000-12-19
*
Réparation de bugs de LoadPath
herbelin
2000-12-15
*
Bug des locaux au premier niveau des modules qui disparaissaient de l'environ...
herbelin
2000-12-15
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Reparation conditions de positivites inductifs, echange dans add_entry
mohring
2000-12-06
*
Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de l...
herbelin
2000-12-05
*
Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de l...
herbelin
2000-12-05
*
caractere opaque des constantes repris en compte
filliatr
2000-12-04
*
load_path_entry structure simplified; field relative_subdir renamed to coq_dirpa
sacerdot
2000-11-29
*
La zone par défaut pour le nommage des modules est Scratch
herbelin
2000-11-29
*
Enregistrement des racines de la bibliothèque
herbelin
2000-11-29
*
Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ch...
herbelin
2000-11-29
*
Les variables doivent persister dans les vo pour HELM
herbelin
2000-11-28
*
Prise en compte du repertoire dans le section path; utilisation de dirpath po...
herbelin
2000-11-28
*
load_module / open_module un tantinet plus rapides
filliatr
2000-11-27
*
Bug dans find_common_hyps_then_abstract en présence de défs locales
herbelin
2000-11-27
*
Bug extract_instance en présence de défs locales
herbelin
2000-11-27
*
Prise en compte des let in dans les instances de globaux
herbelin
2000-11-27
*
Nettoyage
herbelin
2000-11-26
[next]