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 des erreurs non noyau dans Pretype_errors ou Cases; localisation
herbelin
2001-03-11
*
Avancée vers la prise compte des alias dépendants; prise en compte des clau...
herbelin
2001-03-11
*
Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation
herbelin
2001-03-11
*
Pb génération noms Cases + mise en place mécanisme d'histoire du filtrage ...
herbelin
2001-03-05
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
nouvelle implantation de la reduction
barras
2001-03-01
*
uniformisation avec constr des lieurs dans rawterm/pattern
herbelin
2001-02-14
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...
herbelin
2001-02-06
*
Restructuration de classops; évolution en une version mieux intégrée au re...
herbelin
2001-02-05
*
Restructuration de classops; évolution en une version mieux intégrée au re...
herbelin
2001-02-05
*
Reparation reduce_to_mind
mohring
2001-02-01
*
- coqc : option -image
filliatr
2001-02-01
*
Bug localisation des Syntactif Definition
herbelin
2001-01-31
*
Mise en place de la possibilite d'unfolder des variables locales et des const...
filliatr
2001-01-31
*
Prise en compte du let-in dans lookup_*_as_renamed
herbelin
2001-01-30
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Nouveaux bugs instanciation d'evar par des evar
herbelin
2001-01-19
*
Bug environnement
herbelin
2001-01-11
*
Rajout de la restriction de l'instance en cas d'unification de 2 variables ex...
herbelin
2001-01-04
*
Rattrapage d'erreur pour le Case + Eval Compute in pour Definition
delahaye
2001-01-03
*
Bug de contextes
herbelin
2000-12-26
*
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
[prev]
[next]