index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
DĂ©placement du type stack de Reduction vers Closure et utilisation pour accĂ...
herbelin
2000-12-26
*
Pattern sera mieux dans Pretyping; relâchement head_pattern_bound
herbelin
2000-12-26
*
Un nom long pour les variables de section qui font classe ou coercion; réorg...
herbelin
2000-12-25
*
Bug vieux Match
herbelin
2000-12-25
*
Bug prédicat
herbelin
2000-12-25
*
Bug prédicat old Case/Match
herbelin
2000-12-20
*
RĂ©tablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...
herbelin
2000-12-20
*
Export fonction testant si un inductive est un record
herbelin
2000-12-19
*
Amélioration message d'erreur mauvais prédicat
herbelin
2000-12-18
*
Debut de nettoyage de Simpl
mohring
2000-12-18
*
Suppression du warning several default clauses
herbelin
2000-12-16
*
Bug env vis Ă vis du let in
herbelin
2000-12-15
*
Bugs calcul du prédicat des Cases et Case
herbelin
2000-12-15
*
Printer
mohring
2000-12-15
*
Mauvais env donné à new_isevar
herbelin
2000-12-14
*
Oubli test de correction Ă l'instantiation des evars
herbelin
2000-12-14
*
Mise en page
herbelin
2000-12-14
*
LetIn dans Simpl
mohring
2000-12-14
*
Raffinement erreur Wrong Predicate
herbelin
2000-12-14
*
Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases devien...
herbelin
2000-12-14
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Hint Unfold Local + commentaires
mohring
2000-12-12
*
Debut de reparation de simpl
mohring
2000-12-11
*
Bug Cases en presence d'une absence de clause
herbelin
2000-12-05
*
Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypage
herbelin
2000-11-29
*
La table de pré-évaluation des constantes ne doit pas persister au discharge
herbelin
2000-11-27
*
Utilisation de Let In pour les constantes locales, prise en compte des Let In...
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
*
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
*
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
*
print_id, print_sp -> pr_id, pr_sp
herbelin
2000-11-23
*
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...
herbelin
2000-11-22
*
Mieux Ă sa place dans toplevel
herbelin
2000-11-20
*
Utilisation de global_reference dans rawconstr
herbelin
2000-11-20
*
Utilisation de global_reference dans rawconstr
herbelin
2000-11-20
*
Utilisation de global_reference dans rawconstr; blindage pour quand appelé d...
herbelin
2000-11-20
*
Ajout erreur GlobalNotFound
herbelin
2000-11-20
*
Cablage des syntactif defs avec la Nametab des objets
herbelin
2000-11-20
*
Tables des eval_constant devient une Cstmap
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
*
merge_loc
herbelin
2000-11-08
*
Insertion de coercion au milieu des applications partielles et propagation de...
herbelin
2000-11-08
*
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
*
correction Abstract (et make world passe!)
filliatr
2000-11-02
*
suppression des (* open Generic *)
filliatr
2000-11-02
[next]