aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-04-04Files that handle the dialogue with the graphical user-interface pcoq.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1531 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-04deux fichiers (past et ptype) uniquement sous forme de .mlifilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1527 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-03The function filter_by_module, that was previously exported was not thebertot
one that was really needed. I changed it for filter_by_module_from_list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1525 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-03Export a function (build_inductive) that is used in the graphical interface.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1524 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-03Make sure that the COQTOP variable is really used, when it is set.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1523 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-03Make it possible to perform proofs by induction even on non-inductive types,bertot
as long as one provides the induction principle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1522 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-03psyntax.ml4 sous CVSfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1520 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 06:44:43 +0000