aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes
AgeCommit message (Expand)Author
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
2015-01-15Optionally allow eta-conversion during unification for type classes.Matthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-10Give the same argument name for the record binder of type classMatthieu Sozeau
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-06-29Move Params definition in generalize rewriting out of a section so thatMatthieu Sozeau
2014-06-26Export the right modules in Setoid, avoiding anomalies in generalized rewriting.Matthieu Sozeau
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-09Update and start testing rewrite-in-type code.Matthieu Sozeau
2014-05-09Restore implicit arguments of irreflexivity (fixes bug #3305).Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-03-21Using hnf instead of "intro H" for forcing reduction to a product.herbelin
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-08-08Updating headers.herbelin
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 14:01:22 +0000