aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural
Commit message (Expand)AuthorAge
* NPeano improved, subsumes NatOrderedTypeGravatar letouzey2010-02-09
* NSub: a missing lemma (sub usually decreases)Gravatar letouzey2010-02-09
* NBinary improved, contains more, subsumes NOrderedTypeGravatar letouzey2010-02-09
* DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generationGravatar letouzey2010-02-08
* Division in numbers: kills some Include to avoid bad alias Zsucc = ZDiv.Z.Z'.SGravatar letouzey2010-01-29
* NMake (and hence BigN): shiftr, shiftl now in the signature NSigGravatar letouzey2010-01-25
* NMake: several things need not be macro-generatedGravatar letouzey2010-01-25
* Ring31 : a ring structure and tactic for int31Gravatar letouzey2010-01-19
* NMake_gen: fix previous commit (some spaces were critical), remove some more ...Gravatar letouzey2010-01-19
* NMake_gen: no more spaces at end of linesGravatar letouzey2010-01-19
* More improvements of BigN, BigZ, BigQ:Gravatar letouzey2010-01-18
* BigN, BigZ, BigQ: presentation via unique module with both ops and propsGravatar letouzey2010-01-17
* Avoid some more re-declarations of Equivalence instancesGravatar letouzey2010-01-14
* Numbers/.../NDefOps: one more property about ltbGravatar letouzey2010-01-12
* Numbers: some more proofs about sub,add,le,lt for natural numbersGravatar letouzey2010-01-12
* Numbers: two more Local Obligation TacticGravatar letouzey2010-01-12
* Support "Local Obligation Tactic" (now the default in sections).Gravatar msozeau2010-01-11
* Numbers: BigN and BigZ get instantiations of all properties about div and modGravatar letouzey2010-01-08
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Numbers: separation of funs, notations, axioms. Notations via module, without...Gravatar letouzey2010-01-07
* Patch on subtyping check of opaque constants.Gravatar soubiran2010-01-06
* Numbers abstract layer: more Module Type, used especially for divisions.Gravatar letouzey2010-01-05
* Division in Numbers: factorisation of signaturesGravatar letouzey2010-01-05
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
* RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndGravatar letouzey2009-12-18
* A generic euclidean division in Numbers (Still Work-In-Progress)Gravatar letouzey2009-12-15
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
* 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
* Many fixes in unification:Gravatar msozeau2009-05-20
* 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
* 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
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
* 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
* Enhance the BigN and BigZ infrastructure: Gravatar letouzey2008-06-01
* NBigN: proofs that BigN implements axioms of NAxiomsSigGravatar letouzey2008-05-29
* CyclicAxioms: after discussion with Laurent, znz_WW and variants areGravatar letouzey2008-05-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-26 14:39:07 +0000