index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
Age
Commit message (
Expand
)
Author
2001-09-14
Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)
herbelin
2001-09-14
L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...
herbelin
2001-09-14
L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...
herbelin
2001-09-10
Hack pour gérer les univers dans les prédicats de Cases synthétisés
herbelin
2001-09-09
Nettoyage reduce_to_ind et one_step_reduce
herbelin
2001-09-09
Passage aux univers algébriques
herbelin
2001-09-09
Préparation du prétypage à la mise en place d'univers algébriques
herbelin
2001-09-07
Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)
herbelin
2001-09-04
erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies
barras
2001-08-13
bug de Bruijn
herbelin
2001-08-10
Parsing
herbelin
2001-07-24
Bug Simpl
herbelin
2001-07-21
Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...
herbelin
2001-07-21
Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...
herbelin
2001-07-06
Les tables de coercions ne doivent pas survivre aux sections
herbelin
2001-07-06
la conversion ne doit être testé dans evar_conv qu'en absence de evar
herbelin
2001-07-06
has_undefined_isevars était buggé
herbelin
2001-07-05
Débogage discharge des coercions; nettoyage
herbelin
2001-07-04
message Ambiguous paths seulement si verbose
filliatr
2001-07-02
Nettoyage/restructuration des ensembles d'indicateurs de réductions
herbelin
2001-06-29
traitement du let dans red_product (tactique Red)
barras
2001-06-25
Bug dépendances non pertinentes (dû à des K-rédex) dans le type des branc...
herbelin
2001-06-20
Normalisation du predicat synthetise pour les Case
clrenard
2001-06-16
code mort
herbelin
2001-06-12
Ajout d'une normalisation (beta_iota) pour les predicats de Cases inferes aut...
clrenard
2001-05-29
Facilites pour le debogguage des univers.
coq
2001-05-23
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-15
Modification pour passage p-automates
mohring
2001-05-15
Correction bug predicat du Cases (suite)
herbelin
2001-05-12
Bug propagation du predicat des Cases
herbelin
2001-05-10
Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)
herbelin
2001-05-03
Changement de la structure des points fixes
barras
2001-04-25
Bug perte d'alias avec type dependents
herbelin
2001-04-15
Bug affichage ordre des variables d'un pattern
herbelin
2001-04-13
Mise en place d'un test de clauses non utilisees
herbelin
2001-04-10
Bug context incoherent au passage du lambda et du let dans evar_eqappr
herbelin
2001-04-02
bug Fix signalé par Alexandre (even/odd mal interprété)
filliatr
2001-03-29
deux fois $Id$
filliatr
2001-03-28
amelioration de la structure des univers
barras
2001-03-23
amelioration de la consommation memoire de la conversion en eta-expansant
barras
2001-03-15
entetes
filliatr
2001-03-14
Alias suite + bugs divers et variés
herbelin
2001-03-14
Prise en compte des Let dans l'instance des evars
herbelin
2001-03-12
Rien au lieu erreur si plusieurs cas par défaut; quasi-achèvement alias dé...
herbelin
2001-03-11
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-05
Pb génération noms Cases + mise en place mécanisme d'histoire du filtrage ...
herbelin
2001-03-01
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
nouvelle implantation de la reduction
barras
[next]