aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes
AgeCommit message (Expand)Author
2021-03-30Remove the :> type castJim Fehrle
2021-01-08Modify Classes/SetoidDec.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Classes/SetoidClass.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Classes/EquivDec.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Classes/DecidableClass.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Classes/CEquivalence.v to compile with -mangle-namesJasper Hugunin
2020-12-15Catch up to where I was last time.Jasper Hugunin
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
2020-11-04[stdlib] Decidable instance for negationYishuai Li
2020-08-25Modify Classes/CMorphisms.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/CRelationClasses.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/Morphisms.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Classes/RelationClasses.v to compile with -mangle-namesJasper Hugunin
2020-03-19[stdlib] Remove a few `auto with *`Vincent Laporte
2020-03-18Update headers in the whole code base.Théo Zimmermann
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-23Fixing typos - Part 3JPR
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
2019-02-28Fix #7632: Change syntax of autoapply according to the documentation.Théo Zimmermann
2019-02-04Enrich implicits for instancesJasper Hugunin
2019-02-04Merge PR #9386: Pass some files to strict focusing mode.Pierre-Marie Pédrot
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-23Pass some files to strict focusing mode.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-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-14Remove deprecated options from the standard library.Guillaume Melquiond
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
2017-04-28Allow interactive editing of {C,}Morphisms in PGJason Gross
2016-08-17Fix #4978: priorities of Equivalence instancesMatthieu Sozeau
2016-06-28Typeclasses: use once in by clause for typeclass eautoMatthieu Sozeau
2016-06-16setoid_rewrite: fix the Params resolution tacticMatthieu Sozeau
2016-06-16Typeclasses: stdlib fixes for new search algorithmMatthieu Sozeau
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-24Fix handling of arity of definitional classes.Matthieu Sozeau
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-31Put implicits back as in 8.4.Matthieu Sozeau
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-05-12Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)Guillaume Melquiond
2015-04-09Fix instances of universe-polymorphic generalized rewriting to avoidMatthieu Sozeau
2015-01-15Remove typeclass opaque directive, some proofs in the stdlib rely on it being...Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:51:52 +0000