aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/table.ml
AgeCommit message (Collapse)Author
2002-07-16petit bug lors du passage d'hugoletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2887 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Gros Remaniement Extraction:letouzey
* extraction.ml + modulaire (cf extract_type) et + proche theorie (cf feu extract_app) * table.ml filtre les Extract Constant vers types ou terms * extract_env.ml refuse maintenant les Extraction constr. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2886 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07extraction vers schemeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2771 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-11Factorisation de la grammaire pour Extraction Language.letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2522 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-05cas des constructeurs singletons. Messages d'erreur. Revision de ↵letouzey
test_extraction.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2514 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Big commit extraction:letouzey
- Changement de syntaxe (Extraction Language Toplevel/Ocaml/Haskell) - Retour des inductifs singletons et vides dans extraction.ml (extraction.ml -> actions sur le type, mlutil.ml -> conserve le type) - maintenant par defaut Recursive Extraction === Extraction "file" - kill_prop global est fait dans extraction.ml selon typage (a suivre...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2508 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18ote les redondances des entetesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2309 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-14Revolution culturelle: suppression des arguments propletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2189 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-30Reorganisation de Goption. Passage des options l'utilisant en synchroneletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2145 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-26Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ↵letouzey
ETC etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2141 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-24seisme suite. correction bugsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2138 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-24Patch de goption.ml pour faire marcher les options synchrones. Passage des ↵letouzey
options d'extraction en synchrone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2137 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-23suite du seismeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2135 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-22chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les ↵letouzey
options git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2133 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 23:45:23 +0000