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
*
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
*
petit bug avec Extraction Optimize
letouzey
2004-02-13
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
les modifs depuis la 7.4
letouzey
2003-11-12
*
TODO
letouzey
2003-11-12
*
Extraction Module M devient simplement Extraction M
letouzey
2003-11-12
*
le pb du <<.v vu comme module>> engendre maintenant une erreur
letouzey
2003-11-10
*
message informant de l'ecriture d'un fichier extrait
letouzey
2003-11-10
*
révision du traitement des axiomes non réalisés
letouzey
2003-11-10
*
essai d'extraction sous un module
letouzey
2003-11-10
*
factorisation de (recursive) library
letouzey
2003-11-09
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
pour ocamlweb
letouzey
2003-10-06
*
Cacher les .v8
herbelin
2003-10-03
*
traducteur: affiche les commentaires a l'interieur des commandes
barras
2003-09-22
*
bug dans calcul nb d'occurrences
letouzey
2003-09-05
[next]