aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2007-10-03Révision de theories/Logic concernant les axiomes de descriptions.herbelin
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
2007-10-02Fix a problem doing 'make clean' under Winodwsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10165 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-25Changes in Backtrack documentation. More accurate.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10141 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-24Added the documentation for Backtrack and BackTo.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10139 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-19Indication de quel type de constantes est dépliable dans "simpl" (cfherbelin
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
2007-09-18MAJ date copyright docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10127 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-01A word on the measure and wf modifiersmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10110 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-30Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Serverherbelin
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
2007-08-26Add info on measure based defs.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10095 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-22Save IS NOT the same Defined ....msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10084 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-20Erreur de copier/coller dans la section Guardednotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10079 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-13Correction du bug #1635notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10073 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-09Modification de control_only_guard, qui utilise maintenantnotin
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
2007-08-08A better Program documentation. Include it in the generated stdlib doc.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-07Move Program tactics into a proper theories/ directory as they are general ↵msozeau
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
2007-07-26Corrected the reference to glob.dump, which is used to create ↵emakarov
stdlib/index-body.html. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10051 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-25Modifications de la construction de la documentation de la librairienotin
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
2007-07-19Documentation of Program and its tactics, fix enormous interaction bug due ↵msozeau
to bad cache handling. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10032 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13New bootstrapping, improved, Makefile systemcorbinea
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
2007-07-12port de r9968: bug avec les ring calculatoiresbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9982 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-09More natural notation for intro pattern: @a -> ?aglondu
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
2007-07-07If a fixpoint is not written with an explicit { struct ... }, then letouzey
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
2007-07-06Adding a syntax for "n-ary" rewrite: letouzey
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
2007-07-06extension of the rename tactic: the following is now allowed: letouzey
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
2007-07-06New intro pattern "@A", which generates a fresh name based on A.glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9950 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06Documentation related to commit 9948: intropattern {A,B,C} for (A,(B,C))letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9949 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-05documentation of f_equal and revert and case_eq (and ↵letouzey
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
2007-06-19typo faqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9895 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-08Removed an extra \tacindex occurrence for the tactic discriminate.emakarov
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
2007-06-07Ajout doc clear sans argumentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9880 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-17Fixed bug #1540 (typo on name .coqide-gtk2rc)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9828 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-16- MAJ entêtes des fichiers produits par coq_makefileherbelin
- 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
2007-05-11Made some places in the reference manual clearer. Correctedemakarov
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
2007-04-29Ajout possibilité d'options à trois mots.herbelin
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
2007-04-26Documentation de Existential et de Show Existential (fixes bug #1294)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9799 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-18Fixed some typos.glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9789 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-17Corrected a LaTeX typo.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9784 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-17Changed many refman/*.tex files. Put \label and \index commands that ↵emakarov
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
2007-04-16Removed from headers.hva the code to make index point to the sectionemakarov
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
2007-04-12Cleaned doc/common/title.tex file. Increased the space under headersemakarov
in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9758 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-12Standardisation format biblioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9757 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-10Some changes to eliminate Hevea warnings.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9754 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-10Split refman/headers.tex into headers.sty and headers.hva.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9753 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-10Eliminated warning messages from Hevea. Most warning messages wereemakarov
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
2007-04-05Mise en place d'un rafinement de compute. jforest
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
2007-04-04Corrected a typo in doc/refman/Setoid.tex.emakarov
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
2007-03-16Correction du bug #1441notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9712 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-13Correction bug #1439 (comportement de replace by)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9699 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-07Application suggestion #1430 de Yevgeniy pour TEXINPUTSherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9687 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-22doc: typo/english: "is left associating" -> "is left-associative".lmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9671 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 08:43:41 +0000