index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
extraction
/
extraction.ml
Commit message (
Expand
)
Author
Age
*
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
*
nouvelle gestion des constantes de type
letouzey
2003-01-28
*
oubli des add_recursors singleton logiques
letouzey
2003-01-23
*
Extraction des modules, enfin !
letouzey
2003-01-22
*
les empty ind et les singletons etaient oublies par add_recursors
letouzey
2002-12-19
*
une branche de case inutile
letouzey
2002-12-13
*
petit bug
letouzey
2002-12-09
*
chamboulement du codage des indcutifs extraits; deplacements des tables; ...
letouzey
2002-12-09
*
code cleanup (+ debut de commencement de modules)
letouzey
2002-12-05
*
bug pp letin + un inductif constant n'est pas un record
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
*
nettoyage et reorganisation
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
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_type
letouzey
2002-07-24
*
reparation temporaire(?) a coup de MLdummy'
letouzey
2002-07-17
*
Pour ocamlweb
letouzey
2002-07-16
*
Gros Remaniement Extraction:
letouzey
2002-07-16
*
extraction.ml
letouzey
2002-04-08
*
ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ...
letouzey
2002-04-08
*
export de la fonction Reductionops.find_conclusion pour l'extraction
letouzey
2002-04-08
*
reparation du cas des arguments de type qui sont des arités + patch dummy ap...
letouzey
2002-03-28
*
Refonte complete de la génération des types ML
letouzey
2002-03-26
*
un peu moins d'eta-expansion autour des Glob
letouzey
2002-03-20
*
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
*
gros commit: principalement ajout des lambdas arity + leur optimisation en te...
letouzey
2002-03-15
*
cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...
letouzey
2002-03-05
*
Big commit extraction:
letouzey
2002-03-04
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
Test & correction de la production de code Haskell
letouzey
2002-02-12
*
gros changement dans mlutil.ml: ajout d'une elimination globale des prop
letouzey
2002-02-06
*
adaptation de l'extraction aux changements de Christine concernant rec/rect e...
letouzey
2002-01-31
*
maj CHANGES extraction + bug extraction & _
letouzey
2001-12-21
*
Pour ocamlweb ...
letouzey
2001-12-18
*
anti revolution culturelle: retour des arguments logiques
letouzey
2001-12-18
*
compat ocaml 3.03
filliatr
2001-12-13
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
Revolution culturelle: suppression des arguments prop
letouzey
2001-11-14
*
suite refonte extraction.ml
letouzey
2001-11-12
*
Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)
letouzey
2001-11-12
[next]