aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* documentation of commit 10188Gravatar letouzey2007-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10198 85f007b7-540e-0410-9357-904b9bb8a0f7
* Révision de theories/Logic concernant les axiomes de descriptions.Gravatar herbelin2007-10-03
| | | | | | | | Mise à jour du tableau des axiomes dans la FAQ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10170 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a problem doing 'make clean' under WinodwsGravatar notin2007-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changes in Backtrack documentation. More accurate.Gravatar courtieu2007-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10141 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added the documentation for Backtrack and BackTo.Gravatar courtieu2007-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10139 85f007b7-540e-0410-9357-904b9bb8a0f7
* Indication de quel type de constantes est dépliable dans "simpl" (cfGravatar herbelin2007-09-19
| | | | | | | | | message de Benjamin Pierce de sep 2007 sur coq-club) [report de la révision 10128 de la 8.1 vers le trunk] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10129 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ date copyright docGravatar herbelin2007-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10127 85f007b7-540e-0410-9357-904b9bb8a0f7
* A word on the measure and wf modifiersGravatar msozeau2007-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise à jour des paramètres Whelp et ajouts d'options Set Whelp ServerGravatar herbelin2007-08-30
| | | | | | | | | et Set Whelp Getter pour changer le nom des serveurs (report 10105 de la 8.1 vers le trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add info on measure based defs.Gravatar msozeau2007-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10095 85f007b7-540e-0410-9357-904b9bb8a0f7
* Save IS NOT the same Defined ....Gravatar msozeau2007-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10084 85f007b7-540e-0410-9357-904b9bb8a0f7
* Erreur de copier/coller dans la section GuardedGravatar notin2007-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10079 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1635Gravatar notin2007-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10073 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de control_only_guard, qui utilise maintenantGravatar notin2007-08-09
| | | | | | | | | | | | iter_constr_with_full_binders + documentation de Guarded. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M trunk/doc/refman/RefMan-pro.tex M trunk/pretyping/inductiveops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10065 85f007b7-540e-0410-9357-904b9bb8a0f7
* A better Program documentation. Include it in the generated stdlib doc.Gravatar msozeau2007-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move Program tactics into a proper theories/ directory as they are general ↵Gravatar msozeau2007-08-07
| | | | | | purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10060 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrected the reference to glob.dump, which is used to create ↵Gravatar emakarov2007-07-26
| | | | | | stdlib/index-body.html. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications de la construction de la documentation de la librairieGravatar notin2007-07-25
| | | | | | | | | | | | | standard: - ajout d'une entrée dans le Makefile principal pour le fichier de globalisations glob.dump - modifications de doc/Makefile et de l'index html pour gérer les nouveaux fichiers de la librairie standard (en part. ceux dans Ints) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of Program and its tactics, fix enormous interaction bug due ↵Gravatar msozeau2007-07-19
| | | | | | to bad cache handling. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10032 85f007b7-540e-0410-9357-904b9bb8a0f7
* New bootstrapping, improved, Makefile systemGravatar corbinea2007-07-13
| | | | | | | Documented in dev/doc/build-system.txt . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7
* port de r9968: bug avec les ring calculatoiresGravatar barras2007-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9982 85f007b7-540e-0410-9357-904b9bb8a0f7
* More natural notation for intro pattern: @a -> ?aGravatar glondu2007-07-09
| | | | | | | | | | | Caveat about a slight loss of compatibility: Some intro patterns don't need space between them. In particular intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it is still legal but equivalent to intros ?a ?b. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9964 85f007b7-540e-0410-9357-904b9bb8a0f7
* If a fixpoint is not written with an explicit { struct ... }, then Gravatar letouzey2007-07-07
| | | | | | | | | | | | | | | | | | | | | | | | all arguments are tried successively (from left to right) until one is found that satisfies the structural decreasing condition. When the system accepts a fixpoint, it now prints which decreasing argument was used, e.g: plus is recursively defined (decreasing on 1st argument) The search is quite brute-force, and may need to be optimized for huge mutual fixpoints (?). Anyway, writing explicit {struct} is always a possible fallback. N.B. in the standard library, only 4 functions have an decreasing argument different from the one that would be automatically infered: List.nth, List.nth_ok, List.nth_error, FMapPositive.xfind And compiling with as few explicit struct as possible would add about 15s in compilation time for the whole standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a syntax for "n-ary" rewrite: Gravatar letouzey2007-07-06
| | | | | | | | | | | | | | | | | | | | | | rewrite H, H' means: rewrite H; rewrite H'. This should still be compatible with other "features" of rewrite: like orientation, implicit arguments (t:=...), and "in" clause. Concerning the "in" clause, for the moment only one is allowed at the very end of the tactic, and it applies to all the different rewrites that are done. For instance, if someone _really_ wants to use all features at the same time: rewrite H1 with (t:=u), <-H2, H3 in * means: rewrite H1 with (t:=u) in *; rewrite <- H2 in *; rewrite H3 in * git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9954 85f007b7-540e-0410-9357-904b9bb8a0f7
* extension of the rename tactic: the following is now allowed: Gravatar letouzey2007-07-06
| | | | | | | | rename A into B, C into D, E into F. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9952 85f007b7-540e-0410-9357-904b9bb8a0f7
* New intro pattern "@A", which generates a fresh name based on A.Gravatar glondu2007-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9950 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation related to commit 9948: intropattern {A,B,C} for (A,(B,C))Gravatar letouzey2007-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9949 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentation of f_equal and revert and case_eq (and ↵Gravatar letouzey2007-07-05
| | | | | | s/lri.fr/pps.jussieu.fr/ in my bib entry) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9944 85f007b7-540e-0410-9357-904b9bb8a0f7
* typo faqGravatar herbelin2007-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9895 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed an extra \tacindex occurrence for the tactic discriminate.Gravatar emakarov2007-06-08
| | | | | | | Added a tactic "now" which is nonrecursive but generalizes "trivial". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9884 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout doc clear sans argumentGravatar herbelin2007-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9880 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #1540 (typo on name .coqide-gtk2rc)Gravatar herbelin2007-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9828 85f007b7-540e-0410-9357-904b9bb8a0f7
* - MAJ entêtes des fichiers produits par coq_makefileGravatar herbelin2007-05-16
| | | | | | | | - Correction de bugs dans la reconnaissance d'un "*)" potentiel dans les lignes correspondant au mécanisme "section" de coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9826 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made some places in the reference manual clearer. CorrectedGravatar emakarov2007-05-11
| | | | | | | an example about modules that produced a Coq error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9820 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout possibilité d'options à trois mots.Gravatar herbelin2007-04-29
| | | | | | | | | | Suppression au passage syntaxe "Set table field ref", synonyme de "Add table field ref" et de "Unset table field ref", synonyme de "Remove table field ref". Changement de la syntaxe "Test tabel field val" en ""Test tabel field for val". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9810 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation de Existential et de Show Existential (fixes bug #1294)Gravatar notin2007-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed some typos.Gravatar glondu2007-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9789 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrected a LaTeX typo.Gravatar emakarov2007-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9784 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changed many refman/*.tex files. Put \label and \index commands that ↵Gravatar emakarov2007-04-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | immediately follow sectioning commands insides those sectioning commands. If \label{...} is placed after \section{...}, then, when clicking on the link in the HTML file produced by Hevea, we are moved to the correct section, but the section header is just above the screen. Hevea manual recommends writing \section{...\label{...}} and similarly for index. On the other hand, writing commands inside the argument of sectioning commands is potentially dangerous because these arguments are reproduced not only to produce the section header but also to produce headers and/or table of contents entries. Thus, \index{...} and \labels{...} may be executed several times. Indeed, if we put a \typeout{...} instruction inside the argument to a sectioning command then it will be executed, besides the section itself, in the table of contents and once for every appearance of the header. However, it seems that the \label command are not executed several times unless they are prefixed with \protect, and \index command is not executed multiple times even then. So maybe it's OK to put \label and \index inside sectioning commands. When hyperref package is used, the \newlabel command left in .aux file has an extra group {...} which includes another \label command! This may lead to trouble when we use \nameref (?). However, the most reliable way would be to use the optional argument of sectioning commands. Then the text only goes to the optional argument and the text plus \label plus \index goes to the main argument. The optional argument is used for headers and table of contents. This works fine with Hevea as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9781 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed from headers.hva the code to make index point to the sectionGravatar emakarov2007-04-16
| | | | | | | | | labels and not other environment labels (such as enumerate or theorem). This facility was added to Hevea, which is available at http://hevea.inria.fr/distri/unstable/hevea-2007-04-16.tar.gz git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9772 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaned doc/common/title.tex file. Increased the space under headersGravatar emakarov2007-04-12
| | | | | | | in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Standardisation format biblioGravatar herbelin2007-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9757 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some changes to eliminate Hevea warnings.Gravatar emakarov2007-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9754 85f007b7-540e-0410-9357-904b9bb8a0f7
* Split refman/headers.tex into headers.sty and headers.hva.Gravatar emakarov2007-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Eliminated warning messages from Hevea. Most warning messages wereGravatar emakarov2007-04-10
| | | | | | | | | | | | | | from commands about headers; where appropriate, surrounded those by %BEGIN LATEX ... %END LATEX. Removed some \newcommands that were ignored. Removed redefinitions of \land, \lor, \lnot: there are nicely handled by Hevea. Split headers.tex file into headers.sty (for LaTeX) and headers.hva (for Hevea). This allowed removing comments like %BEGIN LATEX and %HEVEA and also commands \makeatletter, \makeatother. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un rafinement de compute. Gravatar jforest2007-04-05
| | | | | | | | | | On peut desormais utiliser: compute delta [f g ...] pour cbv beta iota zera delta [f g ...] et compute delta - [f g ...] pour cbv beta iota zera delta - [f g ...] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9749 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrected a typo in doc/refman/Setoid.tex.Gravatar emakarov2007-04-04
| | | | | | | | | | | Redefined the \index command in doc/refman/headers.tex only for Hevea. Now all sectioning commands (from \part to \subparagraph) store the value of their counter in the command \@indexlabel. It is this command that is used inside the new \index. Thus, the index shows only the the most recent sectioning command, but not \index, \theorem, etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9745 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1441Gravatar notin2007-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1439 (comportement de replace by)Gravatar notin2007-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application suggestion #1430 de Yevgeniy pour TEXINPUTSGravatar herbelin2007-03-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9687 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-04 06:59:33 +0000