aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
Commit message (Expand)AuthorAge
...
* 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
* Simplification of OrdersTac thanks to the functor application ! with no inlineGravatar 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
* Numbers: axiomatization + generic properties of abs and sgn.Gravatar letouzey2010-01-08
* NZAxioms plus a compare allows to build an OrderedTypeGravatar letouzey2010-01-08
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* 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
* "by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ...Gravatar letouzey2010-01-06
* Numbers abstract layer: more Module Type, used especially for divisions.Gravatar letouzey2010-01-05
* Avoid declaring hints about refl/sym/trans of eq in DecidableType2Gravatar letouzey2010-01-05
* Division in Numbers: proofs with less auto (less sensitive to hints, in parti...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
* Division in Numbers : more properties, new filenames based on a paper by R. B...Gravatar letouzey2009-12-17
* Division in Numbers: more properties proved (still W.I.P.)Gravatar letouzey2009-12-16
* A generic euclidean division in Numbers (Still Work-In-Progress)Gravatar letouzey2009-12-15
* NZDomain: investigation of the shape of NZ domain, more results about ofnat:n...Gravatar letouzey2009-12-10
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* Forgot a file in last commit.Gravatar msozeau2009-12-06
* Fix anomaly when using typeclass resolution with filtered hyps in evars.Gravatar msozeau2009-12-06
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
* Diamond-shape instead of linear hiearchy in Numbers/NatIntGravatar letouzey2009-11-18
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
* Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsGravatar letouzey2009-11-16
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-18 13:39:18 +0000