aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* Improved error messages in CoqIDE:Gravatar herbelin2010-11-07
| | | | | | | | | | | - 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
* Add information of localisation when an error involving an "implicitGravatar herbelin2010-11-07
| | | | | | 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
* correcting a non catch error reported as an anomaly (Ploc.Exc)Gravatar jforest2010-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13625 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
* End of commit 13600: files can be given as arguments of coqide again.Gravatar pboutill2010-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13622 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a regression wrt 8.2 when using an "ident" several times in a notationGravatar herbelin2010-11-04
| | | | | | 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
* 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
* Correction bug 2427Gravatar soubiran2010-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13617 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove suspiciously named "implicit" stuff from TermGravatar glondu2010-11-03
| | | | | | | 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
* In Univ, unify order_request and constraint_typeGravatar glondu2010-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add small utility lemmas about nat/P/Z/Q arithmetic.Gravatar letouzey2010-11-02
| | | | | | 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
* 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
* Output universe graph in DOT language if output file ends in .dot or .gvGravatar glondu2010-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13611 85f007b7-540e-0410-9357-904b9bb8a0f7
* More generic Univ.dump_universesGravatar glondu2010-11-02
| | | | | | | | Instead of formatting directly to an output channel, provide an output function that handles formatting and I/O. This allows changing the output format. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13610 85f007b7-540e-0410-9357-904b9bb8a0f7
* NZSqrt : since spec is complete, no need for morphism axiom sqrt_wdGravatar letouzey2010-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13609 85f007b7-540e-0410-9357-904b9bb8a0f7
* NZLog : since spec is complete, no need for morphism axiom log2_wdGravatar letouzey2010-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: misc improvementsGravatar letouzey2010-11-02
| | | | | | | | | - Add alternate specifications of pow and sqrt - Slightly more general pow_lt_mono_r - More explicit equivalence of Plog2_Z and log_inf - Nicer proofs in Zpower git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13607 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
* NArith: a log2 functionGravatar letouzey2010-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13605 85f007b7-540e-0410-9357-904b9bb8a0f7
* NPeano: A log2 function for natGravatar letouzey2010-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13604 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: specs about sqrt and pow of neg numbers, even in NZGravatar letouzey2010-11-02
| | | | | | | These additional specs are useless (but trivially provable) for N. They are quite convenient when deriving properties in NZ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: NZPowProp as a Module Type, some module variable renamingGravatar letouzey2010-11-02
| | | | | | | | | We temporary use a hack to convert a module type into a module Module M := T is refused, so we force an include via Module M := Nop <+ T where Nop is an empty module. To be fixed later more beautifully... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13602 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
* Restored checking that _all_ arguments of the command line are meaningfulGravatar herbelin2010-11-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13600 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add tolerance for existential variables in Check.Gravatar herbelin2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13599 85f007b7-540e-0410-9357-904b9bb8a0f7
* An experimental support for open constrs in hints and in "using"Gravatar herbelin2010-10-31
| | | | | | | option of "auto". Works for not too complicated hints (e.g. "@pair _ _ 0"). Would be simpler if make_apply_entry supported lemmas containing evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13598 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning the use of parentheses around evd and evdref (cosmetic commit).Gravatar herbelin2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13597 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor code improvements around libobjectGravatar herbelin2010-10-31
| | | | | | | | - renamed load_object in mltop into load_ml_object to avoid confusion with load_object in library - flushed the liboject warning in real time git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13596 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor factorization of the part of the code used for Unnamed_thm saving.Gravatar herbelin2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13595 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slight code cleaning in auto.ml (made code of make_exact_entry andGravatar herbelin2010-10-31
| | | | | | make_apply_entry more similar). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slight cosmetic cleaning of tacred.ml.Gravatar herbelin2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13593 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add (quilt's) .pc to .gitignoreGravatar glondu2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some unnecessary (?) "open Ideutils"Gravatar glondu2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13589 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove (unused) ide/highlight.mllGravatar glondu2010-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13588 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction of bug #2414 (report of r 13586)Gravatar jforest2010-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13587 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibility camlp4/camlp5Gravatar herbelin2010-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fail, when successful, prints something only in verbose modeGravatar glondu2010-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13583 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix minor typo in error message (Closes: #2408)Gravatar glondu2010-10-25
| | | | | | Patch from Adam Megacz. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2412, continued (preprocessing of Ltac Debug errorsGravatar herbelin2010-10-23
| | | | | | | forgotten in r13431). Sorry for having thought that the extra needed line could after all be not necessary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13576 85f007b7-540e-0410-9357-904b9bb8a0f7
* Used multiple lists of implicit arguments to transfer the choices ofGravatar herbelin2010-10-23
| | | | | | | | | | Program in terms of implicit arguments to the rest of the library. This commit only covers the case of list of implicit arguments that have a different length in Program (e.g. inl, Vcons) but not the case of implicit arguments which differs only in their maximality status (e.g. pair). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13575 85f007b7-540e-0410-9357-904b9bb8a0f7
* Automatically translate hints of the form "c _ ... _" into "c". BesidesGravatar herbelin2010-10-23
| | | | | | | being convenient, it improves compatibility when moving more implicit arguments to maximal status. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2412 (preprocessing of Ltac Debug errors forgotten in r13431).Gravatar herbelin2010-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13573 85f007b7-540e-0410-9357-904b9bb8a0f7
* FMapFacts: typo noticed by AaronGravatar letouzey2010-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13572 85f007b7-540e-0410-9357-904b9bb8a0f7
* Still another Open Scope than should be LocalGravatar letouzey2010-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13571 85f007b7-540e-0410-9357-904b9bb8a0f7
* Solve name conflict about pow introduced by commit 13546.Gravatar letouzey2010-10-21
| | | | | | | - NPeano isn't Exported by default anymore (contains pow for nat). - in coq_micromega.ml, we specify more where to find the pow of R. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13569 85f007b7-540e-0410-9357-904b9bb8a0f7
* Still some more Cpow in Type rather than Set (cf. r13542)Gravatar letouzey2010-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13568 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 08:15:03 +0000