aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
Commit message (Expand)AuthorAge
* BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)Gravatar letouzey2009-11-12
* Repair interpretation of numeral for BigQ, add a printer (close #2160)Gravatar letouzey2009-11-12
* SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMaxGravatar letouzey2009-11-10
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
* Numbers: finish files NStrongRec and NDefOpsGravatar letouzey2009-11-06
* Numbers: more (syntactic) changes toward new style of type classesGravatar letouzey2009-11-06
* Numbers: start using Classes stuff, Equivalence, Proper, Instance, etcGravatar letouzey2009-11-03
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsGravatar letouzey2009-09-09
* Many fixes in unification:Gravatar msozeau2009-05-20
* Rewrite autorewrite to use a dnet indexed by the left-hand sides (orGravatar msozeau2009-04-14
* Parsing files for numerals (+ ascii/string) moved into pluginsGravatar letouzey2009-03-27
* Cyclic31: proof of a forgotten admitGravatar letouzey2009-02-10
* Uniformity with the rest of the StdLib : _symm --> _symGravatar letouzey2008-12-12
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
* Autour du parsing:Gravatar herbelin2008-07-15
* Fix bug #1899: no more strange notations for Qge and QgtGravatar letouzey2008-07-04
* Various bug fixes in type classes and subtac:Gravatar msozeau2008-07-01
* QMake : alternative equivalences with Qcanon thanks to earlier irreducibility...Gravatar letouzey2008-06-30
* QMake: Proofs that add_norm and other ..._norm functions produce irreducible ...Gravatar letouzey2008-06-28
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
* Some work on BigQ :Gravatar letouzey2008-06-25
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* In abstract parts of theories/Numbers, plus/times becomes add/mul, Gravatar letouzey2008-06-03
* In abstract parts of theories/Numbers, plus/times becomes add/mul, Gravatar letouzey2008-06-02
* newton iteration for sqrt31Gravatar thery2008-06-02
* Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inGravatar letouzey2008-06-01
* BigQ: starting to create and use an interface QSigGravatar letouzey2008-06-01
* Enhance the BigN and BigZ infrastructure: Gravatar letouzey2008-06-01
* NBigN: proofs that BigN implements axioms of NAxiomsSigGravatar letouzey2008-05-29
* Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are Gravatar letouzey2008-05-28
* CyclicAxioms: after discussion with Laurent, znz_WW and variants areGravatar letouzey2008-05-28
* Cyclic31: proofs for addmuldiv31, tail031 and head031. Only two Admitted left !Gravatar letouzey2008-05-28
* Cyclic31: proof of auxiliary function iter_int31 + (failed) attempt at provin...Gravatar letouzey2008-05-27
* Correction du problème de complexité de Print Assumptions :Gravatar aspiwack2008-05-27
* Cyclic31: migrate auxiliary lemmas to their legitimate filesGravatar letouzey2008-05-27
* Cyclic31 : proof of the spec of gcd31Gravatar letouzey2008-05-27
* Int31 : gcd31 was wrongGravatar letouzey2008-05-26
* Cyclic31: cleanup, 2 Admitted killed (6 remaining)Gravatar letouzey2008-05-26
* Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ...Gravatar letouzey2008-05-23
* (Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...Gravatar letouzey2008-05-23
* writing a match on a digit via syntax "if ... then ... else" is not a good id...Gravatar letouzey2008-05-22
* Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...Gravatar letouzey2008-05-22
* QRewrite is now obsolete. It was containing manual ltac stuffGravatar letouzey2008-05-22
* switch theories/Numbers from Set to Type (both the abstract and the bignum pa...Gravatar letouzey2008-05-22
* Minor improvement: group stuff about carry apart from stuff about zn2zGravatar letouzey2008-05-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 14:57:45 +0000