aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets
AgeCommit message (Expand)Author
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-10-05Adapting theories to unused pattern-matching variable warning.Hugo Herbelin
2020-05-01Fixing #11903: Fixpoints not truly recursive in standard library.Hugo Herbelin
2020-04-03Avoiding using a fixed introduction name in Ltac code of stdlib.Hugo Herbelin
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-19[stdlib] Remove a few `auto with *`Vincent Laporte
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-10-22FSetEqProperties: do not use “omega”Vincent Laporte
2019-10-22FSets: do not use “omega”Vincent Laporte
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-05-23Fixing typos - Part 3JPR
2019-04-02Remove -compat 8.7Jason Gross
2019-04-01Several improvements and fixes of LiaFrédéric Besson
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-10-02Update compat notations to be compat 8.7Jason Gross
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-09-10Deprecate romega in favor of lia.Vincent Laporte
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:40:02 +0000