aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Collapse)AuthorAge
* deplacement de l'optimisation inductif singletonGravatar letouzey2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1616 85f007b7-540e-0410-9357-904b9bb8a0f7
* script de bench automatique pour extractionGravatar letouzey2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1615 85f007b7-540e-0410-9357-904b9bb8a0f7
* Making sure there will be no warnings at compile time.Gravatar bertot2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de FieldGravatar delahaye2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1609 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correcting a problem of s that appears behind a Let when there areGravatar bertot2001-04-18
| | | | | | | | | several variables introduced (showproof.ml) Added CASTEDOPENCOMMAND, QUALIDCONSTARG as variants in several places (xlate.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1604 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changing the commands to switch to textual explanation of proofs.Gravatar bertot2001-04-18
| | | | | | | Removing the "Show Dad Rules." command that breaks down parsing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1600 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding files for the production of textual explanations as used in pcoq.Gravatar bertot2001-04-18
| | | | | | | | | | dependence files are updated accordingly. Modifications in other files to cope with a few errors in the translation for the parser (mostly around records, coercions, and the search-pattern command). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1599 85f007b7-540e-0410-9357-904b9bb8a0f7
* eliminiation des singletons du genre sig + diversGravatar letouzey2001-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1587 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle gestion des variables de type MLGravatar letouzey2001-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1583 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentation automatique de la bibliothèque standardGravatar filliatr2001-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
* réparation d'un bug de Correctness: whd_programs ne doit pas réduire les ↵Gravatar filliatr2001-04-11
| | | | | | terms contenant des Evar pas des Metas; mise à jour des exemples git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1577 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug dans eta-expansion des constructeurs. Argument Prop dans extract_type_appGravatar letouzey2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1575 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage exemples Correctness; changement du nom de pred_of_minus dans coq_omegaGravatar filliatr2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1573 85f007b7-540e-0410-9357-904b9bb8a0f7
* réparation Correctness; options Extraction (changement de syntaxe)Gravatar filliatr2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1571 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug lift dans IsRel de extract_type. Axiomes dans extract_typeGravatar letouzey2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1570 85f007b7-540e-0410-9357-904b9bb8a0f7
* exemples CorrectnessGravatar filliatr2001-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1562 85f007b7-540e-0410-9357-904b9bb8a0f7
* branchement extraction en standard (pas de Require)Gravatar filliatr2001-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1561 85f007b7-540e-0410-9357-904b9bb8a0f7
* réparation QuoteGravatar filliatr2001-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout lemmes arithmetiquesGravatar mohring2001-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1557 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make sure the parser knows about the constructors of type nat, soGravatar bertot2001-04-07
| | | | | | | | that specific syntax for this type can be parsed and translated to tree structures. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1555 85f007b7-540e-0410-9357-904b9bb8a0f7
* Two constants had been given in the wrong package (Logic_type instead ofGravatar bertot2001-04-07
| | | | | | | the correct Logic_Type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1554 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction d'un bug de QuoteGravatar filliatr2001-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1553 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4Gravatar filliatr2001-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1551 85f007b7-540e-0410-9357-904b9bb8a0f7
* axiomes dans les typesGravatar filliatr2001-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1549 85f007b7-540e-0410-9357-904b9bb8a0f7
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug ↵Gravatar filliatr2001-04-04
| | | | | | d'ocamldep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1547 85f007b7-540e-0410-9357-904b9bb8a0f7
* implification de extract_constr et extract_termGravatar letouzey2001-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1545 85f007b7-540e-0410-9357-904b9bb8a0f7
* These files are used to construct an independent parser, that is a smallGravatar bertot2001-04-04
| | | | | | | | | coq that is only able to parse coq script files and produced a tree-like representation. For now this representation is only given in a postfix format, but other format (such as XML) could also be possible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1540 85f007b7-540e-0410-9357-904b9bb8a0f7
* These files are loaded coq-interface to make a process that is "pcoq" enabled.Gravatar bertot2001-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make sure the constructors of Z and positive are recognized: they show upGravatar bertot2001-04-04
| | | | | | | when parsing expressions between back-quotes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Files that handle the dialogue with the graphical user-interface pcoq.Gravatar bertot2001-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1531 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentationGravatar filliatr2001-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1530 85f007b7-540e-0410-9357-904b9bb8a0f7
* supression vieux fichiers extractionGravatar filliatr2001-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1529 85f007b7-540e-0410-9357-904b9bb8a0f7
* rollback sur les commandes Extract Constant/Inductive; nettoyage et ↵Gravatar filliatr2001-04-04
| | | | | | documentation code git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1528 85f007b7-540e-0410-9357-904b9bb8a0f7
* deux fichiers (past et ptype) uniquement sous forme de .mliGravatar filliatr2001-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1527 85f007b7-540e-0410-9357-904b9bb8a0f7
* commandes Extract Constant/Inductive; message d'erreur pour les axiomesGravatar filliatr2001-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1526 85f007b7-540e-0410-9357-904b9bb8a0f7
* ménageGravatar filliatr2001-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1521 85f007b7-540e-0410-9357-904b9bb8a0f7
* psyntax.ml4 sous CVSGravatar filliatr2001-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1520 85f007b7-540e-0410-9357-904b9bb8a0f7
* utilisation de Options.if_verboseGravatar filliatr2001-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1519 85f007b7-540e-0410-9357-904b9bb8a0f7
* parenthèses autour des types dans les arguments des constructeursGravatar filliatr2001-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1515 85f007b7-540e-0410-9357-904b9bb8a0f7
* underscores pour les variables représentant des propositionsGravatar filliatr2001-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1514 85f007b7-540e-0410-9357-904b9bb8a0f7
* inductifs videsGravatar filliatr2001-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1513 85f007b7-540e-0410-9357-904b9bb8a0f7
* ml_pop au lieu de ml_lift dans betared_astGravatar filliatr2001-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1512 85f007b7-540e-0410-9357-904b9bb8a0f7
* à faireGravatar filliatr2001-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1511 85f007b7-540e-0410-9357-904b9bb8a0f7
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1509 85f007b7-540e-0410-9357-904b9bb8a0f7
* extraction modulaireGravatar filliatr2001-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1506 85f007b7-540e-0410-9357-904b9bb8a0f7
* extraction modulaire + environnement des Fix corrigéGravatar filliatr2001-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1505 85f007b7-540e-0410-9357-904b9bb8a0f7
* repertoire pour les tests d'extractionGravatar filliatr2001-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1504 85f007b7-540e-0410-9357-904b9bb8a0f7
* application avec bcp argsGravatar letouzey2001-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1503 85f007b7-540e-0410-9357-904b9bb8a0f7
* beta-reductionGravatar filliatr2001-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1502 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place de Correctness (ne compile pas encore)Gravatar filliatr2001-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1501 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 11:49:07 +0000