aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets
Commit message (Expand)AuthorAge
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
* drop vo.itarget files and compute the corresponding the corresponding values ...Gravatar Matej Kosik2017-06-01
* Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\
| * Remove if_then_else. Use tryif instead.Gravatar Théo Zimmermann2016-10-03
* | Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* | Typeclasses: stdlib fixes for new search algorithmGravatar Matthieu Sozeau2016-06-16
* | Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | 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
|/
* ZArith/Int.v: some modernizationsGravatar Pierre Letouzey2015-04-02
* MMapPositive: another implementation of MMapsGravatar Pierre Letouzey2015-03-06
* Forbid Require inside interactive modules and module types.Gravatar Maxime Dénès2014-12-25
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* MSetRBT: unfortunate typo in compare_height (fix #3413)Gravatar Pierre Letouzey2014-07-10
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Avoid using a deprecated lemma in the standard library.Gravatar Guillaume Melquiond2014-06-26
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* 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
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* - Fix arity handling in retyping (de Bruijn bug!)Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Cbn is happier when ?SetPositive fixpoints have the set as recursive argumentGravatar Pierre Boutillier2014-05-02
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
* "Boolean Equality" and "Case Analysis" are already off by default...Gravatar letouzey2013-07-17
* No more constant named "int" in Coq theories (cf bug #2878)Gravatar letouzey2012-12-18
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
* MSetRBT: a tail-recursive plengthGravatar letouzey2012-08-06
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* MSetRBT : elementary arith proofs instead of calls to liaGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* MSetRBT : implementation of MSets via Red-Black treesGravatar letouzey2012-04-13
* MSetAVL: better implementation of filter suggested by X. LeroyGravatar letouzey2012-01-17
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightGravatar letouzey2011-10-14
* fsetdec : non-atomic elements are now transformed as variables first (fix #2464)Gravatar letouzey2011-10-07
* Improved handling of element equalities in fsetdec (fix #2467)Gravatar letouzey2011-10-07
* Modularization of BinInt, related fixes in the 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
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* s/appartness/membership/g (Closes: #2470)Gravatar glondu2011-01-06
* Extraction: re-introduce some eta-expansions in rare situations leading to '_...Gravatar letouzey2010-09-20
* For the moment, two small manual eta-expansions to avoid '_a after extractionGravatar letouzey2010-09-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-16 00:05:28 +0000