aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 11:39:25 +0000