aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
Commit message (Expand)AuthorAge
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Restore implicit arguments of irreflexivity (fixes bug #3305).Gravatar Matthieu Sozeau2014-05-09
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)Gravatar letouzey2012-12-18
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...Gravatar msozeau2012-01-31
* Tentative to fix bug #2628 by not letting intuition break records. Might be t...Gravatar msozeau2012-01-28
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* SearchAbout and similar: add a customizable blacklistGravatar letouzey2011-08-11
* All the parameters of Compare are implicits.Gravatar pboutill2011-07-26
* Follow-up concerning eqb / ltb / leb comparisonsGravatar letouzey2011-06-21
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* Modularization of BinNat + fixes of stdlibGravatar letouzey2011-05-05
* Modularization of BinPos + fixes in StdlibGravatar letouzey2011-05-05
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Fix compilation issues.Gravatar msozeau2011-02-16
* - Fix treatment of globality flag for typeclass instance hints (theyGravatar msozeau2011-02-14
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Integer division: quot and rem (trunc convention) in addition to div and modGravatar letouzey2010-11-10
* Numbers: NZPowProp as a Module Type, some module variable renamingGravatar letouzey2010-11-02
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* FSetPositive: sets of positive inspired by FMapPositive.Gravatar letouzey2010-07-16
* Bool: iff lemmas about or, a reflect inductive, an is_true functionGravatar letouzey2010-07-10
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Uniformisation Sorting/Mergesort and Structures/OrdersGravatar letouzey2010-02-16
* CompSpecType, a clone of CompSpec but in Type instead of PropGravatar letouzey2010-02-12
* NPeano improved, subsumes NatOrderedTypeGravatar letouzey2010-02-09
* NBinary improved, contains more, subsumes NOrderedTypeGravatar letouzey2010-02-09
* ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedTypeGravatar letouzey2010-02-09
* 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
* Try to avoid re-declaring Equivalence, especially for Logic.eqGravatar letouzey2010-01-13
* GenericMinMax: still a min_case_strong with hypothesis in the wrong orderGravatar letouzey2010-01-12
* 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
* Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni...Gravatar letouzey2010-01-07
* OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with...Gravatar letouzey2010-01-07
* DecidableType2+OrderedType2 : notations in specific Module Type, slicing of O...Gravatar letouzey2010-01-07
* misc improvements in some Structures filesGravatar letouzey2010-01-07
* Avoid declaring hints about refl/sym/trans of eq in DecidableType2Gravatar letouzey2010-01-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 02:53:41 +0000