aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-04-03installation des .cmo pour l'extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1518 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-02mise a jour pour ocamlwebfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1517 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-02mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1516 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-04-02bug Fix signalé par Alexandre (even/odd mal interprété)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1510 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30branchement extraction (bytecode seulement)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1509 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30Ajout de lemmes sur les booleensmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1508 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30Introduction d'une preuve de False_recmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1507 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-29mise en place de Correctness (ne compile pas encore)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1501 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-29deux fois $Id$filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1500 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-29fichiers extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1499 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-28amelioration de la structure des universbarras
elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-27Interprétation des qualidargherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1496 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-27mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1494 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-26Bibliotheque Nummohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1491 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-25ocaml 3.01 requisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1488 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-25Tag pour une beta3-ocaml3.01herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1487 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1486 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1485 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23Les règles d'affichage ajoutés dans le commit précédent avait le même ↵herbelin
nom que la règle pour command git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1484 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23amelioration de la consommation memoire de la conversion en eta-expansantbarras
les definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1483 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1482 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-23La strategie de recherche de lookup_eliminator etait insuffisanteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1480 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-22Règle de syntaxe pour CASTEDCOMMANDherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1478 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-22Problèmes de NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1477 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-22Bug MUTCASE au lieu CASEherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1476 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-21option -verbose a coqc; option -i suppriméefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1474 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-15les options passées sont prioritaires sur les -I par défautfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1468 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-26 21:21:38 +0000