aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
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-08Refresh universes in params when generating schemes (Closes: #2429)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13631 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-08Print universes in debugging printersglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13630 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
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
2010-11-07Improved error messages in CoqIDE:herbelin
- add a check that coqtop can be run before starting the interface - returns the error message in case of problem - made illegal option message more informative - use coqtop.byte when coqide.byte (is it a good heuristic?) - made debugging messages silent by default in ide/undo.ml (Ctrl-C was calling Pervasives.prerr_endline instead of Ideutils.prerr_endline) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13627 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-07Add information of localisation when an error involving an "implicitherbelin
types" occurs. Also improved the "unexpected type" error message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13626 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-07correcting a non catch error reported as an anomaly (Ploc.Exc)jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13625 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-04End of commit 13600: files can be given as arguments of coqide again.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13622 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-04Fixing a regression wrt 8.2 when using an "ident" several times in a notationherbelin
in different scopes (backport of r13613 from 8.3 to trunk). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13621 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-03Correction bug 2427soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13617 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-03Remove suspiciously named "implicit" stuff from Termglondu
The lambda_implicit series of functions are used only in Indtypes, so we move them there. In the checker, they are already there... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13615 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-03In Univ, unify order_request and constraint_typeglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13614 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-02Add small utility lemmas about nat/P/Z/Q arithmetic.letouzey
Initial patch by Eelis van der Weegen, minor adaptations by myself git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13613 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-02Output universe graph in DOT language if output file ends in .dot or .gvglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13611 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:09:17 +0000