aboutsummaryrefslogtreecommitdiff
path: root/theories/Structures
AgeCommit message (Expand)Author
2021-03-19Merge PR #13730: Lint stdlib with -mangle-names #6coqbot-app[bot]
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2021-01-08Modify Structures/OrderedType.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Structures/DecidableType.v to compile with -mangle-namesJasper Hugunin
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-08-25Modify Structures/GenericMinMax.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Structures/OrdersFacts.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Structures/OrdersTac.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Structures/Orders.v to compile with -mangle-namesJasper Hugunin
2020-05-04add order properties about boolOlivier Laurent
2020-04-07Integrated changes proposed by @JasonGrossilya
2020-04-07proposed fix for the issue #12015 (String_as_OT)ilya
2020-03-23Fix levels of `<=?` and `<?` in the stdlibJason Gross
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-10-31lia: depend only on ZArith_baseVincent Laporte
2019-10-22OrderedTypeEx: do not use “omega”Vincent Laporte
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-05-01Add PairUsualDecidableTypeFullOliver Nash
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2019-01-23Pass some files to strict focusing mode.Gaëtan Gilbert
2018-12-10Merge PR #7221: The usual order of strings.Hugo Herbelin
2018-11-28Merge PR #7153: Make OrderedTypeFullFacts a module functorGaëtan Gilbert
2018-11-22The usual order of strings.Yao Li
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-04-02Make OrderedTypeFullFacts a module functorSimon Gregersen
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-02-27Update headers following #6543.Théo Zimmermann
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
2017-05-16Stop using auto with * in two proofs.Théo Zimmermann
2016-10-12Little addition to 6eede071 for consistency of style in OrdersFacts.v.Hugo Herbelin
2016-09-17Further "decide equality" tests on demand of Jason.Hugo Herbelin
2016-09-15Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Hugo Herbelin
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
2016-01-13MMaps: remove it from final 8.5 release, since this new library isn't mature ...Pierre Letouzey
2015-12-31Put implicits back as in 8.4.Matthieu Sozeau
2015-12-07Fix some typos.Guillaume Melquiond
2015-03-06MMapPositive: another implementation of MMapsPierre Letouzey
2015-03-05MMaps again : adding MMapList, an implementation by ordered listPierre Letouzey
2015-03-04Introducing MMaps, a modernized FMaps.Pierre Letouzey
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:53:50 +0000