aboutsummaryrefslogtreecommitdiff
path: root/theories/MSets
AgeCommit message (Expand)Author
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-05-23Fixing typos - Part 3JPR
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-08-22Fix typo of caracterisation -> c*h*aracterisationSiddharth Bhat
2018-08-18Merge PR #8272: Fix typo in documentation, heigth --> height.Théo Zimmermann
2018-08-17Fix typo in documentation, heigth --> height.Nick Lewycky
2018-02-27Update headers following #6543.Théo Zimmermann
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 14:41:10 +0000