aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/Extraction.v
Commit message (Expand)AuthorAge
* Factorisation de la grammaire pour Extraction Language.Gravatar letouzey2002-03-11
* Big commit extraction:Gravatar letouzey2002-03-04
* typoGravatar letouzey2001-11-09
* Creation de Recursive Extarction ModuleGravatar letouzey2001-11-03
* Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...Gravatar letouzey2001-10-26
* chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...Gravatar letouzey2001-10-22
* travail sur le Extract ConstantGravatar letouzey2001-09-18
* mise en place extraction haskellGravatar filliatr2001-05-14
* Changement de la structure des points fixesGravatar barras2001-05-03
* réparation Correctness; options Extraction (changement de syntaxe)Gravatar filliatr2001-04-10
* branchement extraction en standard (pas de Require)Gravatar filliatr2001-04-09
* mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4Gravatar filliatr2001-04-05
* commandes Extract Constant/Inductive; message d'erreur pour les axiomesGravatar filliatr2001-04-03
* utilisation de Options.if_verboseGravatar filliatr2001-04-03
* extraction modulaire + environnement des Fix corrigéGravatar filliatr2001-03-30
* changement type_var et signatureGravatar filliatr2001-03-28
* conservation des arguments dans Prop (snif)Gravatar filliatr2001-03-27
* extraction recursive d'un morceau d'environnementGravatar filliatr2001-03-27
* extraction naive de fix et caseGravatar filliatr2001-03-20
* entetesGravatar filliatr2001-03-15
* extraction des types et des inductifsGravatar filliatr2001-02-22
* nouveau design ou le renommage sera fait a posterioriGravatar filliatr2001-02-21