aboutsummaryrefslogtreecommitdiff
path: root/theories/MSets
AgeCommit message (Expand)Author
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-03Remove if_then_else. Use tryif instead.Théo Zimmermann
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-16Typeclasses: stdlib fixes for new search algorithmMatthieu Sozeau
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
2016-04-27Revert "Temporary hack to compensate missing comma while re-printing tactic"Hugo Herbelin
2016-04-27Temporary hack to compensate missing comma while re-printing tacticHugo Herbelin
2015-04-02ZArith/Int.v: some modernizationsPierre Letouzey
2015-03-06MMapPositive: another implementation of MMapsPierre Letouzey
2014-12-25Forbid Require inside interactive modules and module types.Maxime Dénès
2014-10-01Simpl less (so that cbn will not simpl too much)Pierre Boutillier
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-07-10MSetRBT: unfortunate typo in compare_height (fix #3413)Pierre Letouzey
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-06-26Avoid using a deprecated lemma in the standard library.Guillaume Melquiond
2014-06-04Make standard library independent of the names generated byHugo Herbelin
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-05-09Restore implicit arguments of irreflexivity (fixes bug #3305).Matthieu Sozeau
2014-05-06Try a new way of handling template universe levelsMatthieu Sozeau
2014-05-06- Fix arity handling in retyping (de Bruijn bug!)Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-05-02Cbn is happier when ?SetPositive fixpoints have the set as recursive argumentPierre Boutillier
2014-05-02Eta contractions to please cbnPierre Boutillier
2013-07-17"Boolean Equality" and "Case Analysis" are already off by default...letouzey
2012-12-18No more constant named "int" in Coq theories (cf bug #2878)letouzey
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-01Ltac repeat is in fact already doing progressletouzey
2012-08-06MSetRBT: a tail-recursive plengthletouzey
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
2012-07-05MSetRBT : elementary arith proofs instead of calls to lialetouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-04-13MSetRBT : implementation of MSets via Red-Black treesletouzey
2012-01-17MSetAVL: better implementation of filter suggested by X. Leroyletouzey
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-10-14MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightletouzey
2011-10-07fsetdec : non-atomic elements are now transformed as variables first (fix #2464)letouzey
2011-10-07Improved handling of element equalities in fsetdec (fix #2467)letouzey
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
2011-03-17CompareSpec: a slight generalization/reformulation of CompSpecletouzey
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-02-17- Use transparency information all the way through unification andmsozeau
2011-01-06s/appartness/membership/g (Closes: #2470)glondu
2010-09-20Extraction: re-introduce some eta-expansions in rare situations leading to '_...letouzey
2010-09-17For the moment, two small manual eta-expansions to avoid '_a after extractionletouzey
2010-07-22Made notations for exists, exists! and notations of Utf8.v recursive notationsherbelin
2010-07-16MSetPositive: mention MSetInterface instead of FSetInterfaceletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 10:51:43 +0000