aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-10Modified searchPattern. Before this correction, constructors were overlooked,bertot
because the observation was done on the internal data-structure provided in the inductive definition. But this internal data-structure is not well-suited pattern-matching, since it contains debruijn indices where the inductive type should occur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1572 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-10Mise a jour de la config pour distribmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1569 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1568 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10Bug affichage LETPATTERNherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1567 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10Bug context incoherent au passage du lambda et du let dans evar_eqapprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1566 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-09Interdiction des 'Save (thm_tok)? id' si thm pas ouvert par Goalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1565 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-09Uniformisation des 'Save def_tok id'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1564 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-09nettoyage d'entrees de grammaires inutilescourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1563 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-09mise à jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1560 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-09MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1558 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-08ajout des lemmes Zimmermanmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1556 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-06bug Print Proof; usage coqtop/coqcfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1552 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-05array_fold_left_ifilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1550 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-04ajout de coq_example# dans coq-texwerner
BW git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1548 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-04Adding the dependencies for the parser that is used in the interface pcoq.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1546 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-04adding the directives to compile the parser that is used in the graphicalbertot
interface git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1544 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04Added a flag that makes it possible to re-load files while taking only thebertot
pieces of data for which the system is ready, without raising an exception. This is used to construct a reduced-coq process that can only parse. This reduced-coq is a part of the graphical interface pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1543 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04Added two files that are used for the connection with the graphical ↵bertot
user-interface pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1542 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04Add a flag to avoid sending too many warnings when reloading syntax filesbertot
in the parser used for the graphical user-interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1541 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-04Add a Comments command, that does nothing, but is quite useful to to havebertot
well displayed comments in the middle of developments (that is comments that are more than just plain strings). Used in the graphical interface pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1537 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04add the binary coq-interface, used for the communication with the graphicalbertot
user-interface pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1536 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04add the compilation of the files needed for the interface with pcoq.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1535 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04adding entry points for the arguments of the Comment command.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1534 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04Adding A command for comments, this makes it possible to have structuredbertot
comments that will be displayed nicely in structured oriented interfaces like pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1533 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04dependencies required for contrib/interfacebertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1532 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 05:57:41 +0000