index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
extraction
/
extraction.mli
Age
Commit message (
Expand
)
Author
2009-03-20
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2008-11-06
Cosmetic: no more whitespace at end of lines in extraction files
letouzey
2008-02-01
Beaoucoup de changements dans la representation interne des modules.
soubiran
2007-10-17
Major reorganisation of the extraction "backend".
letouzey
2004-11-16
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-07-16
Nouvelle en-tête
herbelin
2003-04-16
BIG MAJ Extraction:
letouzey
2003-01-22
Extraction des modules, enfin !
letouzey
2002-12-09
chamboulement du codage des indcutifs extraits; deplacements des tables; ...
letouzey
2002-12-05
code cleanup (+ debut de commencement de modules)
letouzey
2002-08-02
Modules dans COQ\!\!\!\!
coq
2002-07-16
Gros Remaniement Extraction:
letouzey
2002-03-28
reparation du cas des arguments de type qui sont des arités + patch dummy ap...
letouzey
2002-03-26
Refonte complete de la génération des types ML
letouzey
2002-03-15
gros commit: principalement ajout des lambdas arity + leur optimisation en te...
letouzey
2002-03-05
cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...
letouzey
2002-03-04
Big commit extraction:
letouzey
2001-11-14
Revolution culturelle: suppression des arguments prop
letouzey
2001-11-12
Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)
letouzey
2001-11-05
GROS COMMIT:
barras
2001-04-12
nouvelle gestion des variables de type ML
letouzey
2001-04-04
implification de extract_constr et extract_term
letouzey
2001-04-04
documentation
filliatr
2001-03-30
extraction modulaire + environnement des Fix corrigé
filliatr
2001-03-28
changement type_var et signature
filliatr
2001-03-20
Extract_term_with_type. mise a jour & verification des commentaires
letouzey
2001-03-15
entetes
filliatr
2001-03-14
interface du extract_rec. Extract_constr prend un environnement
letouzey
2001-02-26
ajout Vprop, Tprop et Eprop
filliatr
2001-02-22
extraction des types et des inductifs
filliatr
2001-02-21
nouveau design ou le renommage sera fait a posteriori
filliatr
2001-02-20
mise en place fichiers extraction
filliatr
2001-02-06
mise en place extraction
filliatr