aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.mli
AgeCommit message (Expand)Author
2017-12-27Remove the local polymorphic flag hack.Maxime Dénès
2017-12-27Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...Maxime Dénès
2017-12-13[econstr] Cleanup in `vernac/classes.ml`.Emilio Jesus Gallego Arias
2017-11-30Remove unused boolean from cl_context field of Typeclasses.typeclassGaëtan Gilbert
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-13Make the typeclass implementation fully compatible with universe polymorphism.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Class_tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Typeclasses API using EConstr.Pierre-Marie Pédrot
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-09-09Fast path in Clenvtac.clenv_refine typeclass resolution.Pierre-Marie Pédrot
2016-06-16Typeclasses:rename solve_instantiation* & use HookMatthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-02-16Fix bug #3960: potential evar instance categorized as an unresolvableMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-09-15Rework typeclass resolution and control of backtracking.Matthieu Sozeau
2014-09-11Add a flag for restricting resolution of typeclasses toMatthieu Sozeau
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-07-31Add an option to solve typeclass goals generated by apply which can't beMatthieu Sozeau
2014-05-06- Fix treatment of global universe constraints which should be passed alongMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-08-01Added printing of instance priority to the Print Instances command.ppedrot
2013-06-12One more fix for rewrite: disallow resolving of the (partial) constraintsmsozeau
2013-05-12Use the Hook module here and there.ppedrot
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-18Finer fix for bug 3017, mark unresolvability only of goals that aremsozeau
2012-12-18Modulification of nameppedrot
2012-12-08Finish patch for Hint Resolve, stopping to generate new constant names formsozeau
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-08-08Updating headers.herbelin
2012-06-04Forward-port fixes from 8.4 (15358, 15353, 15333).msozeau
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-03-20Fix interface of resolve_typeclasses: onlyargs -> with_goals:msozeau
2012-03-19Fix bugs related to Program integration.msozeau
2012-03-02Noise for nothingpboutill
2012-01-23Fix for Program Instance not separately checking the resolution of evars of t...msozeau
2011-11-18Restore backward compatibility. ":>" declares subinstances in Class declarati...msozeau
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-10-07Fix bug #2557 and an issue with Propers for complementmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 21:57:12 +0000