aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-12-14Add improved indenters that rely on the current proof state to choose the ↵gmelquio
indentation depth. Patch by Cedric Auger. These two indenters need to be exercised a bit to see if they are actually useful to users. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13715 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-14Add navigation items for quickly moving between word occurrences.gmelquio
Patch by Cedric Auger. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13714 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-14Improved the search/replace dialog box:gmelquio
+-----------------------------------+ | Find: ************** [Find again] | | Replace With: ****** [Repl.&Find] | | [?] Search backward [ Close ] | +-----------------------------------+ Ctrl+b (un)checks "Search backward", Return searches again, Ctrl+r replaces and searches again, Esc close the dialog box. Patch by Cedric Auger. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13713 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-14Fix mutex being released from a different thread than it is acquired from.gmelquio
Needed for FreeBSD. Patch by Cedric Auger. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13712 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-13Remove an unused function with a Evd.fold in subtacletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13711 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-13Goal: preventively replace an Evd.fold by an equivalent Evd.fold_undefinedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13710 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-13Class_tactics: avoid an Evd.fold taking ages in contrib ProjectiveGeometryletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13709 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-13Avoid silent loss of data when closing an unsaved buffer.gmelquio
Patch by David Baelde. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13707 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-12Sorry for the mistake in r13702pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13704 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-10Attempt to preserve casts during a refine, especially VMcastletouzey
placed by vm_cast_no_check git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13703 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-10First release of Vector library.pboutill
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
2010-12-09Don't interpret VMcast as an ordinary type cast in Definition a := t <: T.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13698 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-09In passing, very quick uniformization of coqdoc headers in a few files.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13696 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-09ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2letouzey
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
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-06Fixed status of ÷ and × in coqdoc (they were seen as letter instead of ↵herbelin
symbol). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13691 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-06Use !Pp_control.std_ft for printing grammarsglondu
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
2010-12-04Made new comm. model between coq and coqide support '-R foo ""'-style option.herbelin
This fixes bug #2442. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13683 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-04Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).herbelin
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
2010-12-04Fixing coqdoc pretty-printing of a table in Mergesort. Incidentally,herbelin
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
2010-12-04Better fix to bug #2183 ("moduleid" internal name got exposed to usersherbelin
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
2010-12-04Fixing several bugs with links to notation in coqdoc, including bug #2445:herbelin
- 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
2010-12-03Fixing bug using explictly declared implicit arguments in inductive arities.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13671 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-03Redirect stdout to stderr in -ideslaveglondu
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
2010-12-03Remove dead codeglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13669 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-02Fixing a bug introduced in r12304 (move of interpretation ofherbelin
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
2010-12-02Document new tactics in CHANGESglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13666 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-12-01* Kernel/Term:regisgia
- 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
2010-12-01* Kernel/Termregisgia
Remove an unsound optimization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13661 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-01* Kernel/Termregisgia
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
2010-11-25Dp: minor fix suggested by Virgile Prevostoletouzey
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
2010-11-19CHANGES: mention some changes in trunk since the 8.3 forkletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13655 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-19CHANGES: small re-sync with the one of branch v8.3letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13653 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-18adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13652 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-18Some more revision of {P,N,Z}Arith + bitwise ops in Ndigitsletouzey
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
2010-11-18Do not throw an error for anonymous generalized binders as they will bemsozeau
named after interpretation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13650 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-18NZSqrt: we define sqrt_up, a square root that rounds up instead of down as sqrtletouzey
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
2010-11-18NZLog: we define log2_up, a base-2 logarithm that rounds up instead of down ↵letouzey
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
2010-11-16Support for camlp5 6.02.0 (Closes: #2432)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13642 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-16Division: avoid imposing rem as an infix keyword in Z_scope and bigZ_scope.letouzey
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
2010-11-16Remove redundant clause (and fix compatibility issue)glondu
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
2010-11-16Use full path for unknown stuff in omegaglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13637 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-15Minor fixes from Gregory Malecha. A typo fixed and a better (located) msozeau
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
2010-11-10Oups, fix last commit, a missing file in a vo.itargetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13634 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:52:04 +0000