aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.mli
Commit message (Expand)AuthorAge
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Emilio Jesus Gallego Arias2018-04-26
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | comment "resolvability" bit in Evd.evar_mapGravatar Enrico Tassi2018-02-27
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
* Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...Gravatar Maxime Dénès2017-12-27
|\
* | [econstr] Cleanup in `vernac/classes.ml`.Gravatar Emilio Jesus Gallego Arias2017-12-13
| * Remove unused boolean from cl_context field of Typeclasses.typeclassGravatar Gaëtan Gilbert2017-11-30
|/
* [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Make the typeclass implementation fully compatible with universe polymorphism.Gravatar Pierre-Marie Pédrot2017-07-13
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Class_tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Typeclasses API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
|/
* Fast path in Clenvtac.clenv_refine typeclass resolution.Gravatar Pierre-Marie Pédrot2016-09-09
* Typeclasses:rename solve_instantiation* & use HookGravatar Matthieu Sozeau2016-06-16
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/
* Fix bug #3960: potential evar instance categorized as an unresolvableGravatar Matthieu Sozeau2015-02-16
* Update headers.Gravatar Maxime Dénès2015-01-12
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
* Add a flag for restricting resolution of typeclasses toGravatar Matthieu Sozeau2014-09-11
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Add an option to solve typeclass goals generated by apply which can't beGravatar Matthieu Sozeau2014-07-31
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Added printing of instance priority to the Print Instances command.Gravatar ppedrot2013-08-01
* One more fix for rewrite: disallow resolving of the (partial) constraintsGravatar msozeau2013-06-12
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Finer fix for bug 3017, mark unresolvability only of goals that areGravatar msozeau2013-04-18
* Modulification of nameGravatar ppedrot2012-12-18
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Updating headers.Gravatar herbelin2012-08-08
* Forward-port fixes from 8.4 (15358, 15353, 15333).Gravatar msozeau2012-06-04
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19