aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-oth.tex
AgeCommit message (Collapse)Author
2010-01-28New command Declare Reduction <id> := <conv_expr>.letouzey
Let's avoid writing huge "Eval ... in ..." lines :-) Will be used in particular soon in NMake for defining function via Definition ... := Eval ... in ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12699 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-14Document Local Declare ML Moduleglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12674 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-27Documentation of the Local and Global modifiers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12425 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-26Add doc for [Print Opaque Dependencies] and a better explanation for themsozeau
flags of manual implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12211 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-28Backporting 12112 from v8.2 branch to trunk (fixing documentation bugsherbelin
#2099 in ConstructiveEpsilon.v and #2100 on Global Opaque). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12113 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-14RefMan: a label defined twiceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11978 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-04doc et CHANGES pour la commande Timeoutbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11962 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-01- Fixed bug #2021 (uncaught exception with injection/discriminate whenherbelin
the inductive status of a projectable position comes from a dependency). - Improved doc of the stdlib chapter (see bug #2018), and fixed tex bugs introduced in r11725. - Applied wish #2012 (max_dec transparent). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11728 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-29- Added support for subterm matching in SearchAbout.herbelin
- Backtrack on precise unfolding of "iff" in "tauto": it has effects on the naming of hypotheses (especially when doing "case H" with H of type "{x|P<->Q}" since not unfolding will eventually introduce a name "i" while unfolding will eventually introduce a name "a" (deep sigh). - Miscellaneous (error when a plugin is missing, doc hnf, standardization of names manipulating type constr_pattern, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
of the archive to install in coq user-contrib installation directory. - Relaxed the validity check on identifiers from an error to a warning. - Added a filtering option to Print LoadPath. - Support for empty root in option -R. - Better handling of redundant paths in ml loadpath. - Makefile's: Added target initplugins and added initplugins to coqbinaries. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-29Document native "Declare ML Module"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11523 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
- Extension du test de réversibilité acyclique des notations dures aux notations de type abbréviation (du genre inhabited A := A). - Ajout options Local/Global à Transparent/Opaque. - Retour au comportement 8.1 pour "move" (dependant par défaut et mot-clé dependent retiré). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11472 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
SearchAbout + referring objects by their notation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11446 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-29Lissage de la gestion des chemins de chargement de fichiers :herbelin
- Option -R fait maintenant des Import à tous les niveaux de la hiérarchie de répertoires. Par exemple, Require "Init.Wf" marche. - Option -I rend maintenant possible l'accès aux sous-répertoires via les noms qualifiés. Ainsi -R est exactement comme -I sauf qu'il rend récursivement visibles les noms non qualifiés. - Ajout option -I dir -as coqdir, et par symétrie, -R dir -as coqdir. - Ajout option -exclude-dir pour exclure certains sous-répertoires de la descente récursive de -R. - Amélioration message de localisation pour fichiers venant d'un "state". - Adaptation du checker (et ajout du test check_coq_overwriting qui semblait involontairement oublié dans l'option -R). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11188 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-09- Documentation de admit et Print Assumptions.herbelin
- Relecture, mise à jour, correction d'erreurs et petite réorganisation du chapitre sur les commandes vernaculaires. - Correction bug #1865 (rafraichissement des univers algébriques). - Suppression de la dépendance du initial.coq en les noms longs des fichiers de façons à ce que les dépendances ne soient que purement logique. - Encore un (petit) bug undo ide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22Strategy commands are now exportedbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10971 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-21refined the conversion oraclebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
- vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-03Chgts mineurs:herbelin
- correction commit incorrect d'une modif de test-suite/success/apply.v - réorganisation dev/ - renommage Print Modules en Print Libraries - $Id:$ dans g_vernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10744 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-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-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-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-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
2006-07-12Documentation machine virtuelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9044 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-06Documentation Whelpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9028 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23Nettoyage de l'archive doc et restructuration avant intégration à l'archiveherbelin
principale de Coq et publication des sources (HH) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 21:56:44 +0000