aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Essais dans LtacGravatar delahaye2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1606 85f007b7-540e-0410-9357-904b9bb8a0f7
* make sure the binaries needed for the graphical interface will also beGravatar bertot2001-04-19
| | | | | | | installed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1605 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
* there was a wrong order in the previous version. One was trying toGravatar bertot2001-04-18
| | | | | | | | compile a .vo file before the *.coq files were created. Maybe a missing dependency. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make sure the binaries needed for pcoq are compiled by default.Gravatar bertot2001-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1602 85f007b7-540e-0410-9357-904b9bb8a0f7
* Erreur Makefile JMeqGravatar mohring2001-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1601 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
* *** empty log message ***Gravatar courant2001-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1598 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2001-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1597 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en pageGravatar herbelin2001-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1596 85f007b7-540e-0410-9357-904b9bb8a0f7
* to_constr renvoie directement un constr pour contourner l'ancien ↵Gravatar herbelin2001-04-15
| | | | | | 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
* Suppression de mk_constr qui ne respectait pas l'invariant des applications ↵Gravatar herbelin2001-04-15
| | | | | | (>=1 arg et pas d'imbrication) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug affichage d'implicites pour les vars lieesGravatar herbelin2001-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1593 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug affichage ordre des variables d'un patternGravatar herbelin2001-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1592 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation du bug de TryGravatar delahaye2001-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Non parenthesage des applications de tactiquesGravatar delahaye2001-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un test de clauses non utiliseesGravatar herbelin2001-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1589 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation de l'affichage des THEN'sGravatar delahaye2001-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1588 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
* ajout de testsGravatar mohring2001-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1586 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2001-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1585 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de _ dans les patterns d'introGravatar mohring2001-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1584 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
* Mis un message d'erreur explicite pour l'echec de Elim en casGravatar mohring2001-04-12
| | | | | | | d'incompatibilite de sortes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de l'egalite de John MajorGravatar mohring2001-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1580 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqwebGravatar filliatr2001-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1579 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 rapporte par Randy en Mars 2000Gravatar herbelin2001-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1576 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
* -I contrib/extraction pour compiler Extraction.vGravatar filliatr2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1574 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
* Modified searchPattern. Before this correction, constructors were overlooked,Gravatar bertot2001-04-10
| | | | | | | | | | 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
* 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
* Mise a jour de la config pour distribGravatar mohring2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1569 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1568 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug affichage LETPATTERNGravatar herbelin2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1567 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug context incoherent au passage du lambda et du let dans evar_eqapprGravatar herbelin2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Interdiction des 'Save (thm_tok)? id' si thm pas ouvert par GoalGravatar herbelin2001-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1565 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation des 'Save def_tok id'Gravatar herbelin2001-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1564 85f007b7-540e-0410-9357-904b9bb8a0f7
* nettoyage d'entrees de grammaires inutilesGravatar courant2001-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1563 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
* mise à jourGravatar filliatr2001-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1560 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
* MAJGravatar herbelin2001-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1558 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
* ajout des lemmes ZimmermanGravatar mohring2001-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1556 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 21:34:15 +0000