aboutsummaryrefslogtreecommitdiff
path: root/plugins/nsatz
AgeCommit message (Collapse)Author
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-02Noise for nothingpboutill
Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-12Fix typoglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14893 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-04moins de reification inutile, noatations standardspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14385 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Nsatz: replaced some generic = on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14360 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26Ring2 devient Ncring et la reification par les type classes est partageepottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14298 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-16Tests de nsatz avec la geometriepottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14210 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10ring2, cring, nsatz avec type classe avec parametres plus notationspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14175 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Definitions of positive, N, Z moved in Numbers/BinNums.vletouzey
In the coming reorganisation, the name Z in BinInt will be a module containing all code and properties about binary integers. The inductive type Z hence cannot be at the same location. Same for N and positive. Apart for this naming constraint, it also have advantages : presenting the three types at once is clearer, and we will be able to refer to N in BinPos (for instance for output type of a predecessor function on positive). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14097 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Rename rawterm.ml into glob_term.mlglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 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-02Move stuff about positive into a distinct PArith subdirletouzey
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
2010-07-28unification des tactiques nsatz pour R Z avec celle des anneaux integrespottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13343 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 ↵pottier
85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-27nstaz pour les anneaux integres et les setoides, R Z et Qpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13336 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-12Fix compilation and test-suite of nsatzglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13279 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-08nsatz in an integral domain with specialization to Z and Rpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13265 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-25bug 2328 fixed: failure when polynomial not i idealpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13195 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03Misc fixes related to new nsatz (and ocamlbuild)letouzey
- Kill a warning in ideal.ml corresponding to really brain-dead code. - Restore extraction/vo.otarget in pluginsvo.itarget - In fact, plugins/_tags can be merged into _tags with nice ** patterns - Update .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13062 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03nsatz ajoutepottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13058 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 01:31:23 +0000