aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2001-04-20Ajout des entetesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1641 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20nettoyagefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1639 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Add a treatement of elaborate Intros tactics, CONJPATTERN and family.bertot
This may not be complete, but it already handles simple cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1638 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19scripts; extraction False_recfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1635 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19blindage False_recfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1634 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19cofix; axiomes; eta-expansions pour variables de types mal generalisees (en ↵filliatr
cours) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1633 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19ZArith --> Zarithmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1627 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19synchonization des tables d'extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1626 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19remplace Zarith par ZArithmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1625 85f007b7-540e-0410-9357-904b9bb8a0f7
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-19Making sure there will be no warnings at compile time.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1614 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Ajout de Fielddelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1609 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-18Correcting a problem of s that appears behind a Let when there arebertot
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
2001-04-18Changing the commands to switch to textual explanation of proofs.bertot
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
2001-04-18Adding files for the production of textual explanations as used in pcoq.bertot
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
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-11documentation automatique de la bibliothèque standardfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-11réparation d'un bug de Correctness: whd_programs ne doit pas réduire les ↵filliatr
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
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-10portage exemples Correctness; changement du nom de pred_of_minus dans coq_omegafilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1573 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-09exemples Correctnessfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1562 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-09réparation Quotefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1559 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-08Ajout lemmes arithmetiquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1557 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-07Make sure the parser knows about the constructors of type nat, sobertot
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
2001-04-07Two constants had been given in the wrong package (Logic_type instead ofbertot
the correct Logic_Type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1554 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06correction d'un bug de Quotefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1553 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-04renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug ↵filliatr
d'ocamldep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1547 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-04These files are used to construct an independent parser, that is a smallbertot
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
2001-04-04These files are loaded coq-interface to make a process that is "pcoq" enabled.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1539 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04Make sure the constructors of Z and positive are recognized: they show upbertot
when parsing expressions between back-quotes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1538 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 02:59:19 +0000