aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction
AgeCommit message (Collapse)Author
2001-04-19modifs des scripts de test autofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1621 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19deplacement de l'optimisation inductif singletonletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1616 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19script de bench automatique pour extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1615 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-13eliminiation des singletons du genre sig + diversletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1587 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-12nouvelle gestion des variables de type MLletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1583 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10bug dans eta-expansion des constructeurs. Argument Prop dans extract_type_appletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1575 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10réparation Correctness; options Extraction (changement de syntaxe)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1571 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10bug lift dans IsRel de extract_type. Axiomes dans extract_typeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1570 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-09branchement extraction en standard (pas de Require)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1561 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-05mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1551 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04axiomes dans les typesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1549 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04implification de extract_constr et extract_termletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1545 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04documentationfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1530 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04supression vieux fichiers extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1529 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04rollback sur les commandes Extract Constant/Inductive; nettoyage et ↵filliatr
documentation code git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1528 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-03commandes Extract Constant/Inductive; message d'erreur pour les axiomesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1526 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-03ménagefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1521 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-03utilisation de Options.if_verbosefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1519 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-02parenthèses autour des types dans les arguments des constructeursfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1515 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-02underscores pour les variables représentant des propositionsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1514 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-02inductifs videsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1513 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-02ml_pop au lieu de ml_lift dans betared_astfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1512 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-02à fairefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1511 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30extraction modulairefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1506 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30extraction modulaire + environnement des Fix corrigéfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1505 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30repertoire pour les tests d'extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1504 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30application avec bcp argsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1503 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30beta-reductionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1502 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28changement type_var et signaturefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1498 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-27conservation des arguments dans Prop (snif)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1495 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-27extraction recursive d'un morceau d'environnementfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1493 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-27trace des inductifs sur Propletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1492 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-26cache pour les constantesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1490 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23eta-expansion des constructeurs si necessaire (a posteriori en miniML)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1481 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23suppression des param dans inductifs. suite du Casesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1479 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-21Reecriture du extract_type pour Prod et Lambda. Eta-expansion dans les ↵letouzey
branches des Cases (cf sumbool_rec) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1475 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-20affichage declarations fix + bug extraction sumbool_rec mis a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1473 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-20mlutilfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1472 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-20extraction naive de fix et casefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1471 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-20Extract_term_with_type. mise a jour & verification des commentairesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1470 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-14interface du extract_rec. Extract_constr prend un environnementletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1464 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-13signatures dans le bon ordrefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1459 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-13Finitefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1458 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-13simplification: plus de contexte pour extract_type et contexte simplifié ↵filliatr
pour extract_term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1457 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-13suite de la verification des assert falseletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1456 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12fin du letinletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1451 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12debut let infilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1450 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12mise a jour commentaires'filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1449 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12Commentaires. Verification des assert false. Probleme des types ML arity.letouzey
Correction des dependances pour bin/coq-extraction dans le Makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1448 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 00:02:09 +0000