aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2011-07-07coq_makefile documentation in Refman and -hpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14270 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-04doc/stdlib: Update the list of ZArith filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14255 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-29update of Micromega docfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14248 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-16refman nsatzpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14211 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-06update of the file list in doc/stdlibletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14112 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28Adding "Tactic Notation" in doc index.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14076 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-15Documentation typo.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14008 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-14Add directories in COQPATH to search path.herbelin
This is to allow users to install plugins when coq is installed system-wide. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14001 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-12remove old traces of SearchIsos (never ported to 7.x nor 8.x)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13986 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08@ in index of refman (last request of bug 2494)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13977 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-06Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)herbelin
(backport from 8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13961 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-06Add 'Existing Instances' declaration to declare multiple instances at once.letouzey
This is useful, for example, in declaring the projection of the dependent record bundled form of an unbundled typeclass. Patch submitted by Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13956 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-03Update documentation concerning proofs loading (cf last commit)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13954 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-21Documentation of the timeout tactical (cf r13917)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13921 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-17An option "Set Default Timeout n."letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13916 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Restore documentation of library String which was removed in 2007 (r10049)herbelin
probably inadvertantly since it is not reported in the commit log. (Thanks to Cédric who noticed it.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13877 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-10Remove obsolete TheoryListglondu
This library is no longer used anywhere, and its contents is very... let's say historical... More seriously, many (and presumably the most useful) stuff that used to be there are in List, now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13828 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-12Fix formatting issue in refmanglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13791 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Remove references to -ide option of coqmktopglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13789 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Add "Print Sorted Universes"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13786 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-24Precision in documentation of "decide equality"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13752 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Remove the two-argument variant of "decide equality"glondu
This variant was ignoring its second argument, and didn't exactly respect its documented specification. This is fixed by removing the variant altogether. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13746 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23More precise documentation for instantiateglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13741 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-09Example of a simple ML tactic (Hello world).fkirchne
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13694 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-06Numbers and bitwise functions.letouzey
See NatInt/NZBits.v for the common axiomatization of bitwise functions over naturals / integers. Some specs aren't pretty, but easier to prove, see alternate statements in property functors {N,Z}Bits. Negative numbers are considered via the two's complement convention. We provide implementations for N (in Ndigits.v), for nat (quite dummy, just for completeness), for Z (new file Zdigits_def), for BigN (for the moment partly by converting to N, to be improved soon) and for BigZ. NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in the reversed order (for consistency with the rest of the world): for instance BigN.shiftl 1 10 is 2^10. NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2) on negative numbers. For the moment I've kept it intact, and have just added a Zdiv2' which is truly equivalent to (Zdiv _ 2). To reorganize someday ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-04Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).herbelin
It is in section "My goal is ..., how can I prove it?" of the FAQ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13681 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-02Documentation for tactic constr_eqglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13665 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-02Add tactic has_evar (#2433)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13664 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-02Add tactic is_evar (Closes: #2433)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13663 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-19SearchAbout: who has never been annoyed by the [ ] syntax ?letouzey
Well, hopefully, that belongs to the past: you should now be able to do the very same queries as before, without typing the [ ]. For instance: SearchAbout plus mult. This removal of [ ] is optional, the old syntax is still legal: - for compatibility reasons - for square bracket lovers - for those that have "inside" or "outside" as legal identifier in their development and want to search about them. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13654 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-10Integer division: quot and rem (trunc convention) in addition to div and modletouzey
(floor convention). We follow Haskell naming convention: quot and rem are for Round-Toward-Zero (a.k.a Trunc, what Ocaml, C, Asm do by default, cf. the ex-ZOdiv file), while div and mod are for Round-Toward-Bottom (a.k.a Floor, what Coq does historically in Zdiv). We use unicode ÷ for quot, and infix rem for rem (which is actually remainder in full). This way, both conventions can be used at the same time. Definitions (and proofs of specifications) for div mod quot rem are migrated in a new file Zdiv_def. Ex-ZOdiv file is now Zquot. With this new organisation, no need for functor application in Zdiv and Zquot. On the abstract side, ZAxiomsSig now provides div mod quot rem. Zproperties now contains properties of them. In NZDiv, we stop splitting specifications in Common vs. Specific parts. Instead, the NZ specification is be extended later, even if this leads to a useless mod_bound_pos, subsumed by more precise axioms. A few results in ZDivTrunc and ZDivFloor are improved (sgn stuff). A few proofs in Nnat, Znat, Zabs are reworked (no more dependency to Zmin, Zmax). A lcm (least common multiple) is derived abstractly from gcd and division (and hence available for nat N BigN Z BigZ :-). In these new files NLcm and ZLcm, we also provide some combined properties of div mod quot rem gcd. We also provide a new file Zeuclid implementing a third division convention, where the remainder is always positive. This file instanciate the abstract one ZDivEucl. Operation names are ZEuclid.div and ZEuclid.modulo. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13633 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-05Numbers: axiomatization, properties and implementations of gcdletouzey
- For nat, we create a brand-new gcd function, structural in the sense of Coq, even if it's Euclid algorithm. Cool... - We re-organize the Zgcd that was in Znumtheory, create out of it files Pgcd, Ngcd_def, Zgcd_def. Proofs of correctness are revised in order to be much simpler (no omega, no advanced lemmas of Znumtheory, etc). - Abstract Properties NZGcd / ZGcd / NGcd could still be completed, for the moment they contain up to Gauss thm. We could add stuff about (relative) primality, relationship between gcd and div,mod, or stuff about parity, etc etc. - Znumtheory remains as it was, apart for Zgcd and correctness proofs gone elsewhere. We could later take advantage of ZGcd in it. Someday, we'll have to switch from the current Zdivide inductive, to Zdivide' via exists. To be continued... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13623 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-03Fix typo in "Hint Extern" docglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13618 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-02Document DOT output of universe graphglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13612 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-02Numbers : log2. Abstraction, properties and implementations.letouzey
Btw, we finally declare the original Zpower as the power on Z. We should switch to a more efficient one someday, but in the meantime BigN is proved with respect to the old one. TODO: reform Zlogarithm with respect to Zlog_def git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13606 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-02Move stuff about positive into a distinct PArith subdirletouzey
Beware! after this, a ./configure must be done. It might also be a good idea to chase any phantom .vo remaining after a make clean git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13601 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-11More precise description of boolean ring in doc (see bug #2401)glondu
Also remove misleading example about classical propositional logic in "What does this tactic do?" section. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13523 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-07TeX input method is now supported upstreamvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13514 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-06Remove Explain* vernacsglondu
Basically untouched since 1999. Same fate as VernacGo (r13506). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13510 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-06Remove VernacGoglondu
I agree with Arnaud on this one... Archeology: I could trace it back to r133 (in 1999!), and it was adapted to many big changes, including change of parsing (r2722, in 2002). Maybe it was used by Centaur or something similar once... The only relevant occurrences of "Go" in SVN history (since initial commit in 1999) is that it "semble peu robuste aux erreurs", without a clear specification of what it is supposed to do... Looks like an interesting feature, though, but needs complete rethinking (and documentation) with the new engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13506 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-05(Hopefully) clearer explanation of Ltac's context patternsglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13503 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-03Added multiple implicit arguments rules per name.herbelin
Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]". This should a priori be used with care (it might be a bit disturbing seeing the same constant used with apparently incompatible signatures). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-28Minor fixes of 'make doc'pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13472 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-23Added a section in the documentation of Vernacular commands about ↵aspiwack
Set/Unset/Test. It allowed to document the behaviour of Local and Global on Set and Unset. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13456 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-19Hopefully a fix for #2176 (redirection not understood with some shells)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13437 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-06Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for ↵emakarov
pngtopnm and pnmtops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13401 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28unification des tactiques nsatz pour R Z avec celle des anneaux integrespottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13343 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-27Minor fixes:msozeau
- Document and fix [autounfold] - Fix warning about default Firstorder tactic object not being defined - Fix treatment of implicits in Program Lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13334 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-25Documentation of Set Automatic Coercions Import.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13327 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-22Extension of the recursive notations mechanismherbelin
- Added support for recursive notations with binders - Added support for arbitrary large iterators in recursive notations - More checks on the use of variables and improved error messages - Do side-effects in metasyntax only when sure that everything is ok - Documentation Note: it seems there were a small bug in match_alist (instances obtained from matching the first copy of iterator were not propagated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 14:30:35 +0000