aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Collapse)Author
2008-02-06- Documentation des nouvelles options d'implicites (Set Strongly Strictherbelin
Implicit, Set Maximal Implicit Insertion, Set Reversible Pattern Implicit, Set Printing Implicit Defensive). - Changement de la sémantique de Set Strongly Strict Implicit : il contient maintenant Set Strict Implicit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10520 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-03Add new files theories/Program/Basics.v and theories/Classes/Relations.vmsozeau
for basic functional programming and relation definitions respectively. Classes.Relations also includes the definition of Morphism and instances for the standard morphisms and relations (eq, iff, impl, inverse and complement). The class_setoid.ml4 [setoid_rewrite] tactic has been reimplemented on top of these definitions, hence it doesn't require a setoid implementation anymore. It also generates obligations for missing reflexivity proofs, like the current setoid_rewrite. It has not been tested on large examples but it should handle directions and occurences. Works with in if no obligations are generated at this time. What's missing is being able to rewrite by a lemma instead of a simple hypothesis with no premises. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10502 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-01Unification de TacLetRecIn et TacLetIn. En particulier, on peutherbelin
maintenant écrire des fonctions récursives qui n'ont pas l'apparence d'être fonctionnelle. La sémantique reste toutefois différente. Par exemple, dans Ltac is := let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in i. l'évaluation de i est paresseuse, alors que dans une version non récursive Ltac is := let i := match goal with |- ?A -> ?B => intro | _ => idtac end in i. l'évaluation de i est forte (et échoue sur le "match" qui n'est pas autorisé à retourner une tactique). (note: code mort dans tactics.ml en passant + indexation Implicit Type dans doc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10495 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-31Debug implementation of dependent induction/dependent destruction and ↵msozeau
document it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-31Finish let| implementation and document itmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10489 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-29Added full documentation for mathematical mode (draft version)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10479 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-05Added a note about the ambiguity of the syntax "qualid" in "tacarg"herbelin
(see coq-club message from 3 Jan 2008). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10422 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-05Standardisation du format des références croisées vers Figure, Section, ↵herbelin
Chapter Remplacement pageref par ref parce que pageref n'a pas de sens pour la version HTML git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10421 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-24Doc updatemsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10258 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16 Added the doc for the new Scheme Equality commandvsiles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10225 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-08documentation of commit 10188letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10198 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-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-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-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-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-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-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-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-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
2007-02-22Documentation of tactical "t1 || t2": t2 is executed if t1 fails tolmamane
progress, not only if it fails (i.e. gives an error). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9670 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 06:11:35 +0000