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
*
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
*
correction d'un stack overflow possible (PR#320)
letouzey
2003-08-28
*
Traduction mlnames
herbelin
2003-08-14
*
bug typage du cases/identity: optim off si inductif avec vars
letouzey
2003-07-10
*
renommage des modules 1er niveau en monolithique
letouzey
2003-07-10
*
bug match match
letouzey
2003-07-08
*
enieme correction du nommage modulaire
letouzey
2003-06-12
*
fin de l'affichage des signatures de modules dans les *.ml
letouzey
2003-06-12
*
interaction entre fun/case permut et assert false
letouzey
2003-06-08
*
oups
letouzey
2003-05-30
*
:= dans un record engendre un LetIn qui n'etait pas géré
letouzey
2003-05-29
*
gestion plus fine des beta-redex lineaires (cf nb_occur_match)
letouzey
2003-05-28
*
bug concernant les projecteurs de Record avec args logiques
letouzey
2003-04-28
*
adaptation a Acc_iter
letouzey
2003-04-28
*
Ooops
letouzey
2003-04-17
*
temporaire
letouzey
2003-04-17
*
BIG MAJ Extraction:
letouzey
2003-04-16
*
Extract Constant marche avec les axiomes schémas de types
letouzey
2003-03-25
*
pour coq-ide
letouzey
2003-03-11
*
pour ocamlweb
letouzey
2003-03-11
*
bugs/améliorations trouvés via FTA
letouzey
2003-02-21
*
maj status de l'extraction des modules
letouzey
2003-02-03
*
hack horrible pour renommage dans Modules Types et Functeurs
letouzey
2003-02-03
*
encore un long_kn
letouzey
2003-02-03
*
plus d'environment fixe cur_env mais un environment evolutif
letouzey
2003-02-02
[next]