index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
uniformisation messages d'erreur
filliatr
2000-11-27
*
load_module / open_module un tantinet plus rapides
filliatr
2000-11-27
*
Faut-il mettre la réduction let-in dans la réduction unfold ?
herbelin
2000-11-27
*
Remettre une section dans fast_integer pour contourner un bug de définition ...
herbelin
2000-11-27
*
La bonne modif des Unfold
herbelin
2000-11-27
*
MAJ
herbelin
2000-11-27
*
Bug dans find_common_hyps_then_abstract en présence de défs locales
herbelin
2000-11-27
*
La table de pré-évaluation des constantes ne doit pas persister au discharge
herbelin
2000-11-27
*
Bug extract_instance en présence de défs locales
herbelin
2000-11-27
*
Prise en compte des définitions locales
herbelin
2000-11-27
*
Prise en compte des implicites de locaux à l'affichage
herbelin
2000-11-27
*
On déplie les locaux dans les types plutôt que de les quantifier par un Let
herbelin
2000-11-27
*
Suppression de Unfold inutile et maintenant échouant
herbelin
2000-11-27
*
Prise en compte des let-in dans les fonctions de réduction pour les tactiques
herbelin
2000-11-27
*
Utilisation de Let In pour les constantes locales, prise en compte des Let In...
herbelin
2000-11-27
*
Bug dans la gestion du contexte en présence de Fix dans le calcul de garde
herbelin
2000-11-27
*
Branchement des Local sur des SectionLocalDef
herbelin
2000-11-27
*
Prise en compte des let in dans les instances de globaux
herbelin
2000-11-27
*
Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...
herbelin
2000-11-27
*
Affichage des définitions locales
herbelin
2000-11-27
*
Ajout map_constr_with_full_binders et strong pour Simpl
herbelin
2000-11-27
*
Changement du parseur par défaut dans Syntax
herbelin
2000-11-27
*
Généralisation de constant_opt_value en reference_opt_value
herbelin
2000-11-27
*
Branchement du mécanisme d'instantiation des Evar en présence de définitio...
herbelin
2000-11-27
*
Prise en compte des let-in dans les fonctions de réduction pour les tactiques
herbelin
2000-11-27
*
Bug dans le calcul des dépendances dans add_discharged_constant
herbelin
2000-11-27
*
Nettoyage
herbelin
2000-11-26
*
Appel des constantes globaux par des noms absolus
herbelin
2000-11-26
*
Le nouvel Induction s'appelle NewInduction
herbelin
2000-11-26
*
MAJ
herbelin
2000-11-26
*
Prise en compte qualid
herbelin
2000-11-26
*
Restruration autour de qualidarg
herbelin
2000-11-26
*
Calcul du chemin optimal dans qualid_of_global
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
*
Prise en compte de noms absolus dans la nametab + nettoyage
herbelin
2000-11-26
*
Prise en compte de noms absolus dans la nametab
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
*
MAJ
herbelin
2000-11-24
*
Bug relocation des hypothèses quand les contextes de définitions et d'utili...
herbelin
2000-11-24
*
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
*
Paramètrage de ocamldebug-v7 par configure à partir d'un 'template'
herbelin
2000-11-24
*
MAJ
filliatr
2000-11-24
*
Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab
filliatr
2000-11-24
*
Ajout BEST partout a coqc
filliatr
2000-11-24
*
certains effets disparaissent a la sortie des sections, d'autres non (selon S...
filliatr
2000-11-24
*
resolution implicites dans produits (bug)
filliatr
2000-11-24
[next]