aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets
AgeCommit message (Expand)Author
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-19Fix warning about shadowing a global name.Gaëtan Gilbert
2017-10-05[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Emilio Jesus Gallego Arias
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-16Removing a dummy parameter in some FMapPositive statements.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-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-05Move option_map notation upJason Gross
2016-07-05Restore option_map in FMapFactsJason Gross
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2015-12-07Fix some typos.Guillaume Melquiond
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-09-09- Fix printing and parsing of primitive projections, including the SetMatthieu Sozeau
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-25Grammar: "allowing to" is not proper EnglishJason Gross
2014-08-05More proofs independent of the names generated by induction/elim overHugo Herbelin
2014-07-31Adding a generalized version of fold_Equal to FMapFacts.Pierre Courtieu
2014-06-26Avoid using a deprecated lemma in the standard library.Guillaume Melquiond
2014-06-20Cleanup treatment of template universe polymorphism (thanks to E. TassiMatthieu Sozeau
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-06Fix after merge.Matthieu 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
2013-01-18Unset Asymmetric Patternspboutill
2012-12-18No more constant named "int" in Coq theories (cf bug #2878)letouzey
2012-10-01Ltac repeat is in fact already doing progressletouzey
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-05-15Intuition: temporary(?) restore the unconditional unfolding of notletouzey
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2012-01-31Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...msozeau
2012-01-28Tentative to fix bug #2628 by not letting intuition break records. Might be t...msozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 05:19:52 +0000