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
*
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
*
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
[next]