aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/Extraction.v
AgeCommit message (Expand)Author
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-03-11Factorisation de la grammaire pour Extraction Language.letouzey
2002-03-04Big commit extraction:letouzey
2001-11-09typoletouzey
2001-11-03Creation de Recursive Extarction Moduleletouzey
2001-10-26Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...letouzey
2001-10-22chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...letouzey
2001-09-18travail sur le Extract Constantletouzey
2001-05-14mise en place extraction haskellfilliatr
2001-05-03Changement de la structure des points fixesbarras
2001-04-10réparation Correctness; options Extraction (changement de syntaxe)filliatr
2001-04-09branchement extraction en standard (pas de Require)filliatr
2001-04-05mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4filliatr
2001-04-03commandes Extract Constant/Inductive; message d'erreur pour les axiomesfilliatr
2001-04-03utilisation de Options.if_verbosefilliatr
2001-03-30extraction modulaire + environnement des Fix corrigéfilliatr
2001-03-28changement type_var et signaturefilliatr
2001-03-27conservation des arguments dans Prop (snif)filliatr
2001-03-27extraction recursive d'un morceau d'environnementfilliatr
2001-03-20extraction naive de fix et casefilliatr
2001-03-15entetesfilliatr
2001-02-22extraction des types et des inductifsfilliatr
2001-02-21nouveau design ou le renommage sera fait a posteriorifilliatr