aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-04-15to_constr renvoie directement un constr pour contourner l'ancien ↵herbelin
Term.mk_constr qui ne respectait pas l'invariant des applications (>=1 arg et pas d'imbrication) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1595 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-15Suppression de mk_constr qui ne respectait pas l'invariant des applications ↵herbelin
(>=1 arg et pas d'imbrication) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1594 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-15Bug affichage d'implicites pour les vars lieesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1593 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-15Bug affichage ordre des variables d'un patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1592 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-14Reparation du bug de Trydelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1591 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-14Non parenthesage des applications de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1590 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-13Mise en place d'un test de clauses non utiliseesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1589 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-13Reparation de l'affichage des THEN'sdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1588 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-13ajout de testsmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1586 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-13MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1585 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-12Ajout de _ dans les patterns d'intromohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1584 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-12Mis un message d'erreur explicite pour l'echec de Elim en casmohring
d'incompatibilite de sortes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1581 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-12Ajout de l'egalite de John Majormohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1580 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-11coqwebfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1579 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-11Bug rapporte par Randy en Mars 2000herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1576 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-10-I contrib/extraction pour compiler Extraction.vfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1574 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-30 03:55:07 +0000