index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
Commit message (
Expand
)
Author
Age
*
corrections mineures suite au commit de restructuration du noyau
barras
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...
herbelin
2001-10-12
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Bugs de vérification de la bonne fondation en présence de définitions loca...
herbelin
2001-10-03
*
Correction messages d'erreur
herbelin
2001-10-03
*
repare la perte d'opacite a la fermeture de section
barras
2001-09-21
*
Transparent
barras
2001-09-20
*
Nettoyage des commentaires
herbelin
2001-09-20
*
Compatibilté make doc
herbelin
2001-09-20
*
Romega
mohring
2001-09-20
*
Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...
herbelin
2001-09-19
*
Affichage des dir_path vide
herbelin
2001-09-19
*
Romega/names/Makefile
mohring
2001-09-18
*
exceptions
barras
2001-09-14
*
mauvais rattrapage d'exception
barras
2001-09-14
*
Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...
herbelin
2001-09-10
*
Passage aux univers algébriques
herbelin
2001-09-09
*
Passage aux univers algébriques
herbelin
2001-09-09
*
Suppression de Type_1, inutile, et non prévu dans le modèle des univers alg...
herbelin
2001-09-09
*
Mécanisme pour faire remonter les contraintes de typage sur les variables de...
herbelin
2001-09-09
*
Mécanisme pour faire remonter les contraintes de typage sur les variables de...
herbelin
2001-09-09
*
Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)
herbelin
2001-09-07
*
Version de la reduction dans Closure plus econome en memoire:
barras
2001-09-05
*
erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies
barras
2001-09-04
*
Parsing
herbelin
2001-08-10
*
Ajout add_prefix/add_suffix
herbelin
2001-08-01
*
Comentaire errone.
clrenard
2001-07-23
*
Nettoyage
herbelin
2001-07-21
*
Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...
herbelin
2001-07-21
*
Ajout hashconsing univers
herbelin
2001-07-03
*
Depliage des let-in dans le test de garde
herbelin
2001-07-03
*
Nettoyage/restructuration des ensembles d'indicateurs de réductions
herbelin
2001-07-02
*
Normalisation du predicat synthetise pour les Case
clrenard
2001-06-20
*
Facilites pour le debogguage des univers.
coq
2001-05-29
*
option -quality
filliatr
2001-05-28
*
erreur DeBruijn causant un RecursionNotOnInductiveType quand le type est un Let
letouzey
2001-05-25
*
Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_types
herbelin
2001-05-25
*
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-23
*
Ajout d'une fonction de remplacement d'un sous-terme par un terme.
clrenard
2001-05-15
*
nettoyage extraction
filliatr
2001-05-09
*
Changement de la structure des points fixes
barras
2001-05-03
*
interdiction occ positives ET negatives dans Pattern
werner
2001-04-24
*
reduction des let in dans whd_programs
filliatr
2001-04-23
*
un typage sûr pour Goal et Check
filliatr
2001-04-20
*
to_constr renvoie directement un constr pour contourner l'ancien Term.mk_cons...
herbelin
2001-04-15
*
Suppression de mk_constr qui ne respectait pas l'invariant des applications (...
herbelin
2001-04-15
*
réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...
filliatr
2001-04-11
[next]