aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
Commit message (Expand)AuthorAge
* Revert "Temporary hack to compensate missing comma while re-printing tactic"Gravatar Hugo Herbelin2016-04-27
* Temporary hack to compensate missing comma while re-printing tacticGravatar Hugo Herbelin2016-04-27
* MMaps: remove it from final 8.5 release, since this new library isn't mature ...Gravatar Pierre Letouzey2016-01-13
* Put implicits back as in 8.4.Gravatar Matthieu Sozeau2015-12-31
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* MMapPositive: another implementation of MMapsGravatar Pierre Letouzey2015-03-06
* MMaps again : adding MMapList, an implementation by ordered listGravatar Pierre Letouzey2015-03-05
* Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
* "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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 10:42:39 +0000