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
*
Message inductive large
herbelin
2003-10-28
*
Set devient predicatif par defaut
herbelin
2003-10-28
*
Mise en place d'un mecanisme ne chargeant pas les preuves opaques
herbelin
2003-10-08
*
Correction bug 328
coq
2003-09-23
*
message d'erreur de garde des cofix
barras
2003-09-22
*
bug fix: term reduced in bad env
barras
2003-09-18
*
Mise en place possibilité de définitions locales dans les paramètres des i...
herbelin
2003-09-06
*
Ajout de l'opti des fermeture (mais debranche pour l'instant)
barras
2003-08-06
*
Improved reduction machine with closure: should use less memory
barras
2003-08-05
*
Comparaison de Cases module mind_equiv
coq
2003-06-30
*
*** empty log message ***
courant
2003-06-27
*
Simplification case_info
herbelin
2003-06-10
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...
letouzey
2003-04-16
*
coupage en deux du bloc pas si mutuellement recursif des module_body & co (.....
letouzey
2003-04-16
*
test: un boolean et une fonction check_for_interrupt inseree dans la conversi...
filliatr
2003-04-08
*
*** empty log message ***
barras
2003-03-12
*
*** empty log message ***
courant
2003-01-31
*
Bug 'with Module' corrige
coq
2003-01-22
*
id_of_msid en plus
letouzey
2003-01-22
*
- amelioration des messages d'erreur de la condition de garde
barras
2002-12-18
*
Contexte locale non-vide interdit a la fin d'un module ou module type
coq
2002-12-18
*
Pourquoi normaliser le prédicat du Cases dans le noyau ? (casse la
herbelin
2002-12-10
*
Déplacement du hash-consing vers declare.ml
herbelin
2002-12-10
*
Corrections de gestion des univers et modules + meilleure gestions des noms...
coq
2002-12-09
*
des Set et des Map en plus
letouzey
2002-12-05
*
suppression du champ mind_singl inutilisé dans mutual_inductive_body
letouzey
2002-12-04
*
Corrige un bug de composition de substitutions
coq
2002-12-04
*
Allègement du noyau
herbelin
2002-11-18
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
pattern-matching avec cas inutilise dans closure
barras
2002-10-15
*
Une fonction de moins dans .mli
coq
2002-10-07
*
Lazy manuelles dans le code
coq
2002-10-07
*
Lazy experimentale temporaire...
coq
2002-10-05
*
Comparaisons des types pendant le sous-typage reactive
coq
2002-09-30
*
Activation du hash-consing
herbelin
2002-09-29
*
Hash-consing pour kernel_name
herbelin
2002-09-29
*
Réparation hash_consing
herbelin
2002-09-29
*
La notation with dependante + affichage dependante de moduels corrige
coq
2002-09-20
*
La notation 'with'. L'interpretation - version preliminaire
coq
2002-08-19
*
Pretty-printing preliminaire des modules, commandes
coq
2002-08-19
*
Strengthenning rules for modules + No modules in sections
coq
2002-08-16
*
Renoncement
herbelin
2002-08-13
*
Petites corrections ici et la
coq
2002-08-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
resolution du pb d'efficacite du a Sign.add_named_decl
barras
2002-04-04
*
renommage de l'exception locale Arity
barras
2002-04-03
*
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-04-02
*
*** empty log message ***
mohring
2002-03-29
[next]