aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Remove an unused function with a Evd.fold in subtacGravatar letouzey2010-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13711 85f007b7-540e-0410-9357-904b9bb8a0f7
* Goal: preventively replace an Evd.fold by an equivalent Evd.fold_undefinedGravatar letouzey2010-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13710 85f007b7-540e-0410-9357-904b9bb8a0f7
* Class_tactics: avoid an Evd.fold taking ages in contrib ProjectiveGeometryGravatar letouzey2010-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13709 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid silent loss of data when closing an unsaved buffer.Gravatar gmelquio2010-12-13
| | | | | | Patch by David Baelde. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sorry for the mistake in r13702Gravatar pboutill2010-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13704 85f007b7-540e-0410-9357-904b9bb8a0f7
* Attempt to preserve casts during a refine, especially VMcastGravatar letouzey2010-12-10
| | | | | | placed by vm_cast_no_check git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13703 85f007b7-540e-0410-9357-904b9bb8a0f7
* First release of Vector library.Gravatar pboutill2010-12-10
| | | | | | | | | | To avoid names&notations clashs with list, Vector shouldn't be "Import"ed but one can "Import Vector.VectorNotations." to have notations. SetoidVector at least remains to do. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7
* Don't interpret VMcast as an ordinary type cast in Definition a := t <: T.Gravatar herbelin2010-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13698 85f007b7-540e-0410-9357-904b9bb8a0f7
* In passing, very quick uniformization of coqdoc headers in a few files.Gravatar herbelin2010-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13696 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2Gravatar letouzey2010-12-09
| | | | | | | | | | | | | | | Now we have: - Zdiv and Zdiv2 : round toward bottom, no easy sign rule, remainder of a/2 is 0 or 1, operations related with two's-complement Zshiftr. - Zquot and Zquot2 : round toward zero, Zquot2 (-a) = - Zquot2 a, remainder of a/2 is 0 or Zsgn a. Ok, I'm introducing an incompatibility here, but I think coherence is really desirable. Anyway, people using Zdiv on positive numbers only shouldn't even notice the change. Otherwise, it's just a matter of sed -e "s/div2/quot2/g". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13695 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
* Fixed status of ÷ and × in coqdoc (they were seen as letter instead of ↵Gravatar herbelin2010-12-06
| | | | | | symbol). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13691 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
* Use !Pp_control.std_ft for printing grammarsGravatar glondu2010-12-06
| | | | | | With camlp5 6.02.1, this fixes "Print Grammar" in coqide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13687 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made new comm. model between coq and coqide support '-R foo ""'-style option.Gravatar herbelin2010-12-04
| | | | | | This fixes bug #2442. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13683 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
* Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).Gravatar herbelin2010-12-04
| | | | | | | Thanks to Marc Lasson for the analysis of the problem and for the initial patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing coqdoc pretty-printing of a table in Mergesort. Incidentally,Gravatar herbelin2010-12-04
| | | | | | | this fixes #2441 (even though some other problem was involved too that r16673 might have solved). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13677 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better fix to bug #2183 ("moduleid" internal name got exposed to usersGravatar herbelin2010-12-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | in coqdoc index files). Bug #2183 was fixed by changing "module" into "moduleid" in Index.type_name instead of changing "moduleid" into "module". But "moduleid" is used for building the html indexes what led to not very nice output (one would expect to see "module" in the index). Apparently, the reason "moduleid" was used instead of "module" as internal name for rendering module in the TeX output of coqdoc was that there were already an old \coqdocmodule historically introduced by Jean-Christophe to format libraries. But this \coqdocmodule seems to have been replaced by a \coqlibrary by Matthieu in r11065. So I conclude that Jean-Christophe's use of \coqdocmodule in coqdoc.sty is definitively obsolete, that the \coqmodule LaTeX command is free for other uses and that \coqdocmoduleid has no reason not to be called \coqdocmodule, and consequently, module has no reason to be some moduleid in Index.type_name. Moreover, it remained a \moduleid in Output.module_ref ? Shouldn't it be \coqdocmoduleid (or actually \coqdocmodule, since the id suffix is apparently no longer needed). Hoping I'm not doing something wrong. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing several bugs with links to notation in coqdoc, including bug #2445:Gravatar herbelin2010-12-04
| | | | | | | | | | | | | | | | | | - single quotes in notations were breaking coqdoc, even raising an out-of-bound error when appearing in the last character of the notation; - letter "x" in notation tokens were inelegantly surrounded by single quotes, - rare, but allowed characters < 32 were lost in index pages. A new fully injective space-free-and-human-readable encoding algorithm is adopted which put single quotes around all terminal tokens, double existing single quotes, and replace invisible characters by ^X-like strings. Moreover, the keywords "Local"/"Global" were blocking the detection of keywords starting coq lines (e.g. "Local Notation" was not recognized as a notation). "Local" and "Global" are now uniformly treated as modifiers of vernac commands as they are in the Coq parser. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13673 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug using explictly declared implicit arguments in inductive arities.Gravatar herbelin2010-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Redirect stdout to stderr in -ideslaveGravatar glondu2010-12-03
| | | | | | | | | This fixes "Print Grammar" in coqide, which uses a camlp5 function that prints to stdout, interfering with the ide-slave communication. Camlp5 should additionnally provide a way to print to a formatter instead of directly using stdout... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13670 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove dead codeGravatar glondu2010-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13669 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a bug introduced in r12304 (move of interpretation ofGravatar herbelin2010-12-02
| | | | | | | | | | | Local/Global modifiers in interpretation loop so as to support Local/Global for grammar extension) that made use of DuringSyntaxChecking error wrapper inappropriately nested with the DuringCommandInterp error wrapper, what disturbed the error processors. Good thing, we can now simplify things and completely remove the DuringSyntaxChecking wrapper. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13667 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document new tactics in CHANGESGravatar glondu2010-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13666 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
* * Kernel/Term:Gravatar regisgia2010-12-01
| | | | | | | | | - Fix a bug in [comp_term] (casts were ignored). - Improve the efficiency of hash table lookup. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13662 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Kernel/TermGravatar regisgia2010-12-01
| | | | | | | | Remove an unsound optimization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13661 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Kernel/TermGravatar regisgia2010-12-01
| | | | | | | | Fix an efficiency bug when hash-consing deep [constr]s. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13660 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dp: minor fix suggested by Virgile PrevostoGravatar letouzey2010-11-25
| | | | | | | Non-dependent products in formulas were turned into implications, leading to some issues. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13656 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: mention some changes in trunk since the 8.3 forkGravatar letouzey2010-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13655 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
* CHANGES: small re-sync with the one of branch v8.3Gravatar letouzey2010-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13653 85f007b7-540e-0410-9357-904b9bb8a0f7
* adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6Gravatar letouzey2010-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Initial plan was only to add shiftl/shiftr/land/... to N and other number type, this is only partly done, but this work has diverged into a big reorganisation and improvement session of PArith,NArith,ZArith. Bool/Bool: add lemmas orb_diag (a||a = a) and andb_diag (a&&a = a) PArith/BinPos: - added a power function Ppow - iterator iter_pos moved from Zmisc to here + some lemmas - added Psize_pos, which is 1+log2, used to define Nlog2/Zlog2 - more lemmas on Pcompare and succ/+/* and order, allow to simplify a lot some old proofs elsewhere. - new/revised results on Pminus (including some direct proof of stuff from Pnat) PArith/Pnat: - more direct proofs (limit the need of stuff about Pmult_nat). - provide nicer names for some lemmas (eg. Pplus_plus instead of nat_of_P_plus_morphism), compatibility notations provided. - kill some too-specific lemmas unused in stdlib + contribs NArith/BinNat: - N_of_nat, nat_of_N moved from Nnat to here. - a lemma relating Npred and Nminus - revised definitions and specification proofs of Npow and Nlog2 NArith/Nnat: - shorter proofs. - stuff about Z_of_N is moved to Znat. This way, NArith is entirely independent from ZArith. NArith/Ndigits: - added bitwise operations Nand Nor Ndiff Nshiftl Nshiftr - revised proofs about Nxor, still using functional bit stream - use the same approach to prove properties of Nand Nor Ndiff ZArith/BinInt: huge simplification of Zplus_assoc + cosmetic stuff ZArith/Zcompare: nicer proofs of ugly things like Zcompare_Zplus_compat ZArith/Znat: some nicer proofs and names, received stuff about Z_of_N ZArith/Zmisc: almost empty new, only contain stuff about badly-named iter. Should be reformed more someday. ZArith/Zlog_def: Zlog2 is now based on Psize_pos, this factorizes proofs and avoid slowdown due to adding 1 in Z instead of in positive Zarith/Zpow_def: Zpower_opt is renamed more modestly Zpower_alt as long as I dont't know why it's slower on powers of two. Elsewhere: propagate new names + some nicer proofs NB: Impact on compatibility is probably non-zero, but should be really moderate. We'll see on contribs, but a few Require here and there might be necessary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13651 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not throw an error for anonymous generalized binders as they will beGravatar msozeau2010-11-18
| | | | | | | named after interpretation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13650 85f007b7-540e-0410-9357-904b9bb8a0f7
* NZSqrt: we define sqrt_up, a square root that rounds up instead of down as sqrtGravatar letouzey2010-11-18
| | | | | | Some more results about sqrt. Similar results for sqrt_up. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13649 85f007b7-540e-0410-9357-904b9bb8a0f7
* NZLog: we define log2_up, a base-2 logarithm that rounds up instead of down ↵Gravatar letouzey2010-11-18
| | | | | | | | as log2 Some more results about log2. Similar results for log2_up. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13648 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support for camlp5 6.02.0 (Closes: #2432)Gravatar glondu2010-11-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13642 85f007b7-540e-0410-9357-904b9bb8a0f7
* Division: avoid imposing rem as an infix keyword in Z_scope and bigZ_scope.Gravatar letouzey2010-11-16
| | | | | | | | | | | No infix notation "rem" for Zrem (that will probably become Z.rem in a close future). This way, we avoid conflict with people already using rem for their own need. Same for BigZ. We still use infix rem, but only in the abstract layer of Numbers, in a way that doesn't inpact the rest of Coq. Btw, the axiomatized function is now named rem instead of remainder. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13640 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove redundant clause (and fix compatibility issue)Gravatar glondu2010-11-16
| | | | | | | This clause should not be needed since Loc.Exc_located = Ploc.Exc is matched a few lines earlier... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13638 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use full path for unknown stuff in omegaGravatar glondu2010-11-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13637 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes from Gregory Malecha. A typo fixed and a better (located) Gravatar msozeau2010-11-15
| | | | | | | error message in case of unnammed record parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13635 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups, fix last commit, a missing file in a vo.itargetGravatar letouzey2010-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13634 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
* Refresh universes in params when generating schemes (Closes: #2429)Gravatar glondu2010-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13631 85f007b7-540e-0410-9357-904b9bb8a0f7
* Print universes in debugging printersGravatar glondu2010-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13630 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
| | | | | | | before the message is delivered to the user. Should avoid useless computation in heavily backtracking tactics (auto, try, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13628 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-27 20:39:05 +0000