aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
Commit message (Collapse)AuthorAge
* suppression de l'archive cvs d'un bout de debugGravatar letouzey2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3462 85f007b7-540e-0410-9357-904b9bb8a0f7
* les empty ind et les singletons etaient oublies par add_recursorsGravatar letouzey2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3461 85f007b7-540e-0410-9357-904b9bb8a0f7
* stupide inlining des construsteursGravatar letouzey2002-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3454 85f007b7-540e-0410-9357-904b9bb8a0f7
* debut de parcours des modulesGravatar letouzey2002-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3432 85f007b7-540e-0410-9357-904b9bb8a0f7
* une branche de case inutileGravatar letouzey2002-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3431 85f007b7-540e-0410-9357-904b9bb8a0f7
* ppGravatar letouzey2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3390 85f007b7-540e-0410-9357-904b9bb8a0f7
* petit bugGravatar letouzey2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3389 85f007b7-540e-0410-9357-904b9bb8a0f7
* chamboulement du codage des indcutifs extraits; deplacements des tables; ...Gravatar letouzey2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3388 85f007b7-540e-0410-9357-904b9bb8a0f7
* reorganisation des recherches de ref dans ml_declGravatar letouzey2002-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3381 85f007b7-540e-0410-9357-904b9bb8a0f7
* code cleanup (+ debut de commencement de modules)Gravatar letouzey2002-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3380 85f007b7-540e-0410-9357-904b9bb8a0f7
* la table PARAMETER n'existe plus (mergé dans la table CONSTANT)Gravatar letouzey2002-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3369 85f007b7-540e-0410-9357-904b9bb8a0f7
* 2 bugs: 1) projections pas renommées 2) mutual fixpoints a l'enversGravatar letouzey2002-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3345 85f007b7-540e-0410-9357-904b9bb8a0f7
* cosmetiqueGravatar letouzey2002-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remaniement du pp, suite: vers un renommage modulaire correcteGravatar letouzey2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3336 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite et fin des records avec ocamlGravatar letouzey2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3325 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug pp letin + un inductif constant n'est pas un recordGravatar letouzey2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3324 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-OupsGravatar letouzey2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3323 85f007b7-540e-0410-9357-904b9bb8a0f7
* OupsGravatar letouzey2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3322 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganisation du pretty-print:Gravatar letouzey2002-11-28
| | | | | | | | | | | - Dfix sans rename_global - question du renommage - code cleanup (plein) Encore a finir: bug modules/qualification et syntax records git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3321 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction des Record, suiteGravatar letouzey2002-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3309 85f007b7-540e-0410-9357-904b9bb8a0f7
* debut de support des records camlGravatar letouzey2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3287 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bug n°191Gravatar letouzey2002-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3285 85f007b7-540e-0410-9357-904b9bb8a0f7
* cleanup table.ml + erreur si Extraction Inline sous sectionGravatar letouzey2002-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3284 85f007b7-540e-0410-9357-904b9bb8a0f7
* remaniement de test_extraction.vGravatar letouzey2002-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3256 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
| | | | | | | | | | | | | | | - Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
* cosmetiqueGravatar letouzey2002-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3210 85f007b7-540e-0410-9357-904b9bb8a0f7
* un bug concernant l'expansion des Map_rec si Map n'est pas ouvertGravatar letouzey2002-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3209 85f007b7-540e-0410-9357-904b9bb8a0f7
* nettoyage et reorganisationGravatar letouzey2002-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3208 85f007b7-540e-0410-9357-904b9bb8a0f7
* maj avec tous les mliGravatar letouzey2002-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3207 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un fichier a utiliser via Drop pour le debug de l'extraction.Gravatar letouzey2002-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3206 85f007b7-540e-0410-9357-904b9bb8a0f7
* L'extraction c'est magic cvs -n upGravatar letouzey2002-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy manuelles dans le codeGravatar coq2002-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy experimentale temporaire...Gravatar coq2002-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite chgt liés aux modulesGravatar letouzey2002-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_typeGravatar letouzey2002-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2913 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation temporaire(?) a coup de MLdummy'Gravatar letouzey2002-07-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2895 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar letouzey2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour ocamlwebGravatar letouzey2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Souci avec example fbidon...Gravatar letouzey2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2888 85f007b7-540e-0410-9357-904b9bb8a0f7
* petit bug lors du passage d'hugoGravatar letouzey2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2887 85f007b7-540e-0410-9357-904b9bb8a0f7
* Gros Remaniement Extraction:Gravatar letouzey2002-07-16
| | | | | | | | | * 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
* extraction vers schemeGravatar letouzey2002-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; ↵Gravatar herbelin2002-06-05
| | | | | | rparation de la protection contre les clauses indiscernables de TACTIC EXTEND et VERNAC COMMAND EXTEND; rparation des grammaires de Extraction, EAuto, TextMode, KillProof et Derive Dependent Inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵Gravatar herbelin2002-05-29
| | | | | | 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
* Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vGravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2720 85f007b7-540e-0410-9357-904b9bb8a0f7
* petit bug dans les noms de fichiersGravatar letouzey2002-04-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2662 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar letouzey2002-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2657 85f007b7-540e-0410-9357-904b9bb8a0f7
* maj doc extraction dans repertoire contrib/extractionGravatar letouzey2002-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2643 85f007b7-540e-0410-9357-904b9bb8a0f7
* maj test des realsGravatar letouzey2002-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2636 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 13:05:52 +0000