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
...
*
plus d'environment fixe cur_env mais un environment evolutif
letouzey
2003-02-02
*
fignolage
letouzey
2003-01-30
*
pb d'hier resolu. Recommit
letouzey
2003-01-30
*
apres le backtrack precedent, remise de trois points precis et surs
letouzey
2003-01-29
*
Ca a tout pété -> Bactrack a la version d'hier
letouzey
2003-01-29
*
affichage module et module type
letouzey
2003-01-29
*
affichage module et module type
letouzey
2003-01-29
*
affichage module et module type
letouzey
2003-01-29
*
workaround en attendant traitement reel des modules types
letouzey
2003-01-28
*
amelioration du pretty-print des modules
letouzey
2003-01-28
*
nouvelle gestion des constantes de type
letouzey
2003-01-28
*
oubli des add_recursors singleton logiques
letouzey
2003-01-23
*
maj V7.4
letouzey
2003-01-23
*
petit bug pp haskell
letouzey
2003-01-22
*
Extraction des modules, enfin !
letouzey
2003-01-22
*
Export M + Module M <: SIG
coq
2003-01-09
*
suppression de l'archive cvs d'un bout de debug
letouzey
2002-12-19
*
les empty ind et les singletons etaient oublies par add_recursors
letouzey
2002-12-19
*
stupide inlining des construsteurs
letouzey
2002-12-18
*
debut de parcours des modules
letouzey
2002-12-13
*
une branche de case inutile
letouzey
2002-12-13
*
pp
letouzey
2002-12-09
*
petit bug
letouzey
2002-12-09
*
chamboulement du codage des indcutifs extraits; deplacements des tables; ...
letouzey
2002-12-09
*
reorganisation des recherches de ref dans ml_decl
letouzey
2002-12-05
*
code cleanup (+ debut de commencement de modules)
letouzey
2002-12-05
*
la table PARAMETER n'existe plus (mergé dans la table CONSTANT)
letouzey
2002-12-03
*
2 bugs: 1) projections pas renommées 2) mutual fixpoints a l'envers
letouzey
2002-11-29
*
cosmetique
letouzey
2002-11-29
*
Remaniement du pp, suite: vers un renommage modulaire correcte
letouzey
2002-11-28
*
suite et fin des records avec ocaml
letouzey
2002-11-28
*
bug pp letin + un inductif constant n'est pas un record
letouzey
2002-11-28
*
Re-Oups
letouzey
2002-11-28
*
Oups
letouzey
2002-11-28
*
Reorganisation du pretty-print:
letouzey
2002-11-28
*
Extraction des Record, suite
letouzey
2002-11-27
*
debut de support des records caml
letouzey
2002-11-26
*
correction bug n°191
letouzey
2002-11-25
*
cleanup table.ml + erreur si Extraction Inline sous section
letouzey
2002-11-25
*
remaniement de test_extraction.v
letouzey
2002-11-18
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
cosmetique
letouzey
2002-11-05
*
un bug concernant l'expansion des Map_rec si Map n'est pas ouvert
letouzey
2002-11-04
*
nettoyage et reorganisation
letouzey
2002-11-04
*
maj avec tous les mli
letouzey
2002-11-04
*
Un fichier a utiliser via Drop pour le debug de l'extraction.
letouzey
2002-11-04
*
L'extraction c'est magic cvs -n up
letouzey
2002-10-31
*
Lazy manuelles dans le code
coq
2002-10-07
*
Lazy experimentale temporaire...
coq
2002-10-05
*
suite chgt liés aux modules
letouzey
2002-09-24
[prev]
[next]