aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* More precise documentation for instantiateGravatar glondu2010-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13741 85f007b7-540e-0410-9357-904b9bb8a0f7
* Example of a simple ML tactic (Hello world).Gravatar fkirchne2010-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13694 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
| | | | | | | | | | | | | | | | | | | | | | | 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
* Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).Gravatar herbelin2010-12-04
| | | | | | 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
* Documentation for tactic constr_eqGravatar glondu2010-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13665 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add tactic has_evar (#2433)Gravatar glondu2010-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13664 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add tactic is_evar (Closes: #2433)Gravatar glondu2010-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13663 85f007b7-540e-0410-9357-904b9bb8a0f7
* SearchAbout: who has never been annoyed by the [ ] syntax ?Gravatar letouzey2010-11-19
| | | | | | | | | | | | | | 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
* Integer division: quot and rem (trunc convention) in addition to div and modGravatar letouzey2010-11-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (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
* Numbers: axiomatization, properties and implementations of gcdGravatar letouzey2010-11-05
| | | | | | | | | | | | | | | | | | | - 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
* Fix typo in "Hint Extern" docGravatar glondu2010-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document DOT output of universe graphGravatar glondu2010-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13612 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers : log2. Abstraction, properties and implementations.Gravatar letouzey2010-11-02
| | | | | | | | | | 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
* Move stuff about positive into a distinct PArith subdirGravatar letouzey2010-11-02
| | | | | | | 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
* More precise description of boolean ring in doc (see bug #2401)Gravatar glondu2010-10-11
| | | | | | | 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
* TeX input method is now supported upstreamGravatar vgross2010-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13514 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove Explain* vernacsGravatar glondu2010-10-06
| | | | | | 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
* Remove VernacGoGravatar glondu2010-10-06
| | | | | | | | | | | | | | | | 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
* (Hopefully) clearer explanation of Ltac's context patternsGravatar glondu2010-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13503 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
| | | | | | | | | 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
* Minor fixes of 'make doc'Gravatar pboutill2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13472 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a section in the documentation of Vernacular commands about ↵Gravatar aspiwack2010-09-23
| | | | | | 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
* Hopefully a fix for #2176 (redirection not understood with some shells)Gravatar herbelin2010-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13437 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for ↵Gravatar emakarov2010-09-06
| | | | | | pngtopnm and pnmtops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13401 85f007b7-540e-0410-9357-904b9bb8a0f7
* unification des tactiques nsatz pour R Z avec celle des anneaux integresGravatar pottier2010-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13343 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes:Gravatar msozeau2010-07-27
| | | | | | | | | - 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
* Documentation of Set Automatic Coercions Import.Gravatar herbelin2010-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13327 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
| | | | | | | | | | | | | - 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
* FSetPositive: sets of positive inspired by FMapPositive.Gravatar letouzey2010-07-16
| | | | | | | | | | Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant. I've also included a MSets version, hence FSetPositive might become soon a mere wrapper for MSetPositive, as for other FSets implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating reference manual credits: gb is now nsatz.Gravatar herbelin2010-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13271 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update of documentation for the standard library (cf. #2332)Gravatar letouzey2010-06-28
| | | | | | This is a slightly modified version of the patch proposed in #2332 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13209 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying François' patches about Canonical Projections (see #2302 and #2334).Gravatar herbelin2010-06-26
| | | | | | | Printer pr_cs_pattern is kept in recordops only. Also updated CHANGES. Fixed spelling of "uniform inheritance condition" in doc too (see git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13204 85f007b7-540e-0410-9357-904b9bb8a0f7
* modifs de nsatz suggerees par HugoGravatar pottier2010-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13194 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une feuille de style pour les définitions spécifiques à Hevea + ↵Gravatar notin2010-06-23
| | | | | | divers corrections sur la génération du manuel de référence. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ↵Gravatar notin2010-06-23
| | | | | | coq.inria.fr) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13185 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of clear dependent and revert dependentGravatar letouzey2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update of Extraction documentationGravatar letouzey2010-06-14
| | | | | | | | | | | | - Removal of the notice about the "experimental" status of extraction. Of course extraction is still experimental, but no less than the rest of Coq ;-) - Removal of the example about heapsort now that Heap is obsolete. - Euclid isn't the best of the examples, but for the moment we leave it - We mention ExtrOcamlIntConv and the others extraction/*.v - Various small improvements git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13136 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction Implicit: documentationGravatar letouzey2010-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.Gravatar herbelin2010-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13114 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a very old (from V6.3) typo in headers.styGravatar herbelin2010-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".Gravatar herbelin2010-06-08
| | | | | | | | | | | | | | | | Updated documentation in many ways: - merged binder and binderlet as done for a while in implementation - fixed a few technical problems (bad indexation of {x:A|P x}, missing spaces in html code in many situations due to missing curly brackets around TeX macros - e.g. around \ldots -, missing dots at end of sentences, ...) - renamed "statement" commands into "assertion" commands and "declaration" commands into "assumption" commands - moved Goal and Save out of the Gallina chapter - avoid some recovering in the Gallina and proof mode chapters - slight smoothing of some hard-to-read paragraphs of the manual git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting part of r12970 to trunk (deprecation of double induction).Gravatar herbelin2010-06-07
| | | | | | Backport of the part of r12970 about Fixpoint doc will come in a further commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13081 85f007b7-540e-0410-9357-904b9bb8a0f7
* doc Nstaz updatedGravatar pottier2010-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13073 85f007b7-540e-0410-9357-904b9bb8a0f7
* A new command Compute foo, shortcut for Eval vm_compute in fooGravatar letouzey2010-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13070 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout oublieGravatar pottier2010-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13057 85f007b7-540e-0410-9357-904b9bb8a0f7
* plugin groebner updated and renamed as nsatz; first version of the doc of ↵Gravatar pottier2010-06-03
| | | | | | nsatz in the refman git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fix in doc chapter on inference rules (added a missing space).Gravatar herbelin2010-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extract Inductive is now possible toward non-inductive types (e.g. nat => int)Gravatar letouzey2010-05-21
| | | | | | | | | | | For instance: Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n => if n=0 then fO () else fS (n-1))". See Extraction.v for more details and caveat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13025 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove compile-command pragmas for emacsGravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | These declarations (e.g. make -C .. bin/coqtop.byte) are quite annoying when debugging stuff over the whole archive: all of a sudden, M-x recompile isn't doing what you intended just because you've visited some specific files. Instead: - Feel free to rather add intermediate targets in the Makefile if they aren't there yet. - For avoiding typing the -C with many .. after, you can have a look at my recursively-descending make: http://www.pps.jussieu.fr/~letouzey/download/make.sh which is to be renamed make and placed in a bin dir with more priority than /usr/bin. Beware! I've already add a few bad surprises with this hack, but it's really convenient nonetheless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13014 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some ocamldoc comments + Fixing name of .coqrc.version file in refmanGravatar pboutill2010-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13013 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 03:46:55 +0000