index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
typeclasses.mli
Age
Commit message (
Expand
)
Author
2018-06-27
Swapping Context and Constr: defining declarations on constr in Constr.
Hugo Herbelin
2018-06-12
[api] Misctypes removal: miscellaneous aliases.
Emilio Jesus Gallego Arias
2018-05-30
Move interning the [hint_pattern] outside the Typeclasses hooks.
Gaëtan Gilbert
2018-05-04
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-04-26
[api] Move `hint_info_expr` to `Typeclasses`.
Emilio Jesus Gallego Arias
2018-03-05
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-02-27
comment "resolvability" bit in Evd.evar_map
Enrico Tassi
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-12-27
Remove the local polymorphic flag hack.
Maxime Dénès
2017-12-27
Merge 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-30
Remove unused boolean from cl_context field of Typeclasses.typeclass
Gaë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-13
Make the typeclass implementation fully compatible with universe polymorphism.
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-04-01
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-02-14
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
Class_tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Typeclasses API using EConstr.
Pierre-Marie Pédrot
2016-11-03
Lets Hints/Instances take an optional pattern
Matthieu Sozeau
2016-09-09
Fast path in Clenvtac.clenv_refine typeclass resolution.
Pierre-Marie Pédrot
2016-06-16
Typeclasses:rename solve_instantiation* & use Hook
Matthieu Sozeau
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-11
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2015-02-16
Fix bug #3960: potential evar instance categorized as an unresolvable
Matthieu Sozeau
2015-01-12
Update headers.
Maxime Dénès
2014-09-15
Rework typeclass resolution and control of backtracking.
Matthieu Sozeau
2014-09-11
Add a flag for restricting resolution of typeclasses to
Matthieu Sozeau
2014-08-25
instanciation is French, instantiation is English
Jason Gross
2014-07-31
Add an option to solve typeclass goals generated by apply which can't be
Matthieu Sozeau
2014-05-06
- Fix treatment of global universe constraints which should be passed along
Matthieu Sozeau
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-03-05
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2013-08-01
Added printing of instance priority to the Print Instances command.
ppedrot
2013-06-12
One more fix for rewrite: disallow resolving of the (partial) constraints
msozeau
2013-05-12
Use the Hook module here and there.
ppedrot
2013-04-29
Merging Context and Sign.
ppedrot
2013-04-29
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-18
Finer fix for bug 3017, mark unresolvability only of goals that are
msozeau
2012-12-18
Modulification of name
ppedrot
2012-12-08
Finish patch for Hint Resolve, stopping to generate new constant names for
msozeau
2012-10-26
Change Hint Resolve, Immediate to take a global reference as argument
msozeau
2012-08-08
Updating headers.
herbelin
2012-06-04
Forward-port fixes from 8.4 (15358, 15353, 15333).
msozeau
2012-05-29
remove many excessive open Util & Errors in mli's
letouzey
2012-05-29
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
[next]
