index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
extraction
Commit message (
Expand
)
Author
Age
*
Suite au mail de Lionel a propos du Makefile:
letouzey
2007-01-12
*
un saut de ligne ...
letouzey
2007-01-12
*
suite de la reparation du bug 1239: apres les inds, les records et vars de types
letouzey
2007-01-05
*
reparation bug 1239
letouzey
2006-12-17
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
Correction bug #1211
notin
2006-10-04
*
Correction bug 1172 + correction en passant de la taille des paramètres de f...
herbelin
2006-07-07
*
oups: il faut penser a fermer la porte en partant (d'un fixpoint)
letouzey
2006-06-09
*
changements de dernieres minutes pour la 8.1 beta:
letouzey
2006-06-09
*
reparation bug 1006
letouzey
2006-06-08
*
debut de reparation du test d'extraction
letouzey
2006-06-02
*
reparation bug #1128
letouzey
2006-06-01
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...
notin
2006-04-28
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)
letouzey
2006-04-20
*
Remplacement Pp.qs par Pptactic.qsnew
herbelin
2005-12-28
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...
herbelin
2005-12-26
*
Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...
herbelin
2005-12-21
*
amelioration de l'extraction haskell: affichage du type des fonctions, et sup...
letouzey
2005-12-16
*
multiples ameliorations de l'extraction scheme:
letouzey
2005-12-16
*
Changement des named_context
gregoire
2005-12-02
*
amelioration de la generation des unsafeCoerce
letouzey
2005-12-01
*
evite certaines eta-expansions cavalieres
letouzey
2005-11-30
*
correctif pour que type t = M.t contienne bien son M.
letouzey
2005-11-29
*
merci les warnings de 3.09 ...
letouzey
2005-11-17
*
Types inductifs parametriques
mohring
2005-11-02
*
Sur le conseil de X.Leroy: x=[||] devient Array.length x=0
letouzey
2005-08-19
*
Standardisation of function names about global references (especially, renami...
herbelin
2005-02-18
*
HUGE COMMIT
sacerdot
2005-01-03
*
travail sur les types extraits
letouzey
2004-12-09
*
When a reference to a constructor is met its inductive type must be closed.
sacerdot
2004-11-18
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
un paquet de corrections de bugs
letouzey
2004-10-04
*
reparation des Extract Constant avec Haskell
letouzey
2004-09-06
*
Nouvelle en-tête
herbelin
2004-07-16
*
ajout des unsafeCoerce + 2 bugs haskell
letouzey
2004-07-14
*
Modules et Records: gros changements pour prendre en compte le nouveau mind_r...
letouzey
2004-06-28
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
correction rapide du bug PR\#592
letouzey
2004-04-05
*
me = andouille
letouzey
2004-03-25
*
Selon les optims, le let-in peut avoir maintenant des args
letouzey
2004-03-25
*
nouvelle commande Set Extraction Flag: reglage fins des optims
letouzey
2004-03-24
*
meme correction de bug, en moins bourrin
letouzey
2004-03-23
*
PolyList -> List
letouzey
2004-03-22
*
correction d'un bug faisant inliner minus, mult, ...
letouzey
2004-03-22
*
petit rajeunissement du test d'extraction
letouzey
2004-03-20
*
Mise en place temporaire d'un afficheur de 'language' pour le traducteur
herbelin
2004-03-13
[next]