index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
extraction
/
table.ml
Age
Commit message (
Expand
)
Author
2009-03-20
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-01-22
Extraction Library works now when some files share the same short name (fix #...
letouzey
2008-12-16
Extraction Blacklist : a new command for avoiding conflicts with existing files
letouzey
2008-11-06
Cosmetic: no more whitespace at end of lines in extraction files
letouzey
2008-11-05
Better extraction renaming phase (fix #1914 plus other non-reported bugs)
letouzey
2008-10-21
warning message when a qualid to extract can be both a module or a cst
letouzey
2008-07-20
Extraction: better dependency computation (after optimisations)
letouzey
2007-12-06
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-10-21
An error message instead of an empty extraction when the monolithic
letouzey
2007-10-17
Major reorganisation of the extraction "backend".
letouzey
2007-10-09
Extraction now checks that the required libraries are indeed loaded (bug #1144)
letouzey
2007-10-09
forbid extraction under a module type
letouzey
2007-10-09
Extract Inline/Inductive/Constant can now be used from inside a module
letouzey
2007-10-08
Better use of tables for storing results of extract_ind (bug #1709)
letouzey
2006-10-28
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-04
Correction bug #1211
notin
2005-01-03
HUGE COMMIT
sacerdot
2004-12-09
travail sur les types extraits
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
2004-06-28
Modules et Records: gros changements pour prendre en compte le nouveau mind_r...
letouzey
2004-03-25
me = andouille
letouzey
2004-03-24
nouvelle commande Set Extraction Flag: reglage fins des optims
letouzey
2003-11-10
le pb du <<.v vu comme module>> engendre maintenant une erreur
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-10-07
Correction du bug 335 et Export/Require Export dans un module
coq
2003-04-28
bug concernant les projecteurs de Record avec args logiques
letouzey
2003-04-16
BIG MAJ Extraction:
letouzey
2003-03-25
Extract Constant marche avec les axiomes schémas de types
letouzey
2003-02-21
bugs/améliorations trouvés via FTA
letouzey
2003-02-02
plus d'environment fixe cur_env mais un environment evolutif
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-11-28
Remaniement du pp, suite: vers un renommage modulaire correcte
letouzey
2002-11-26
debut de support des records caml
letouzey
2002-11-25
cleanup table.ml + erreur si Extraction Inline sous section
letouzey
2002-08-02
Modules dans COQ\!\!\!\!
coq
2002-07-16
petit bug lors du passage d'hugo
letouzey
2002-07-16
Gros Remaniement Extraction:
letouzey
2002-06-07
extraction vers scheme
letouzey
2002-05-29
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-03-11
Factorisation de la grammaire pour Extraction Language.
letouzey
2002-03-05
cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...
letouzey
2002-03-04
Big commit extraction:
letouzey
2001-12-18
ote les redondances des entetes
letouzey
2001-12-13
compat ocaml 3.03
filliatr
2001-11-14
Revolution culturelle: suppression des arguments prop
letouzey
2001-11-05
GROS COMMIT:
barras
[next]