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
*
Refonte complete de la génération des types ML
letouzey
2002-03-26
*
reparation du test des reals
letouzey
2002-03-21
*
considerations de pretty-print
letouzey
2002-03-21
*
deux fichiers supplementaires de customisation d'extraction
letouzey
2002-03-21
*
changement du test extraction suite aux modif inining
letouzey
2002-03-21
*
modification de l'auto-inlining
letouzey
2002-03-21
*
renversement du renommage des variables
letouzey
2002-03-20
*
reparation du controle de l'apparition des termes
letouzey
2002-03-20
*
reorganisation des simplifications: letin eta-expansé apres le kill-dummy
letouzey
2002-03-20
*
un peu moins d'eta-expansion autour des Glob
letouzey
2002-03-20
*
bug optimize_fix fait trop tot
letouzey
2002-03-19
*
suite bug Dglob constant
letouzey
2002-03-19
*
bug avec les MLglob vraiment constants
letouzey
2002-03-19
*
travail sur les stratégies de réduction
letouzey
2002-03-19
*
remplacement des deux constants prop/arity par une seule dummy + pretty-print...
letouzey
2002-03-19
*
epsilon
letouzey
2002-03-15
*
un peu de mise a jour de la doc extraction
letouzey
2002-03-15
*
evite les clash avec le type ocaml unit
letouzey
2002-03-15
*
gros commit: principalement ajout des lambdas arity + leur optimisation en te...
letouzey
2002-03-15
*
Factorisation de la grammaire pour Extraction Language.
letouzey
2002-03-11
*
cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...
letouzey
2002-03-05
*
Big commit extraction:
letouzey
2002-03-04
*
modifs des preambules d'extraction modulaire
letouzey
2002-02-27
*
pretty print des Cases devenant des let-in
letouzey
2002-02-25
*
suite et fin (?) de haskell: gestion des modules, mise en place du'un test
letouzey
2002-02-15
*
debut de gestion des open pour extraction modulaire
letouzey
2002-02-15
*
qq inline manuels (sigS_rec ...) + utilisation de library_part
letouzey
2002-02-14
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
suppression de la condition de la permutation case/fun
letouzey
2002-02-12
*
pretty print
letouzey
2002-02-12
*
Test & correction de la production de code Haskell
letouzey
2002-02-12
*
un assert false de trop (MLexn peut avoir des args)
letouzey
2002-02-07
*
oubli
letouzey
2002-02-06
*
gros changement dans mlutil.ml: ajout d'une elimination globale des prop
letouzey
2002-02-06
*
Ajout d'optimisations locales kill_prop
letouzey
2002-02-05
*
adaptation de l'extraction aux changements de Christine concernant rec/rect e...
letouzey
2002-01-31
*
extraction des CoInductives via les Lazy d'ocaml
letouzey
2002-01-31
*
maj CHANGES extraction + bug extraction & _
letouzey
2001-12-21
*
debranchement du test sur les Reals
letouzey
2001-12-19
*
Pour ocamlweb ...
letouzey
2001-12-18
*
typo de parenthèsage + suppression de string (= str maintenant)
letouzey
2001-12-18
*
anti revolution culturelle: retour des arguments logiques
letouzey
2001-12-18
*
ote les redondances des entetes
letouzey
2001-12-18
*
compat ocaml 3.03
filliatr
2001-12-13
*
correction de bugs concernant la gestion des modules. debranchement du test d...
letouzey
2001-12-10
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
remise au gout du jour du repertoire theories/Sorting de la V6.3
letouzey
2001-11-21
*
hack temporaire concernant les remarks/modules
letouzey
2001-11-20
*
iota généralisé
letouzey
2001-11-20
*
Revolution culturelle: suppression des arguments prop
letouzey
2001-11-14
[next]