| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2012-05-29 | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey |
| 2012-03-20 | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau |
| 2012-03-19 | Fix bugs related to Program integration. | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-01-23 | Fix for Program Instance not separately checking the resolution of evars of t... | msozeau |
| 2011-11-18 | Restore backward compatibility. ":>" declares subinstances in Class declarati... | msozeau |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-10-07 | Fix bug #2557 and an issue with Propers for complement | msozeau |
| 2011-04-13 | - Make typeclass transparency information directly available | msozeau |
| 2011-03-13 | - Add modulo_delta_types flag for unification to allow full | msozeau |
| 2011-03-11 | Keep information on which fields are subclasses in class declarations, | msozeau |
| 2011-02-14 | - Fix treatment of globality flag for typeclass instance hints (they | msozeau |
| 2010-12-15 | Misc improvements about evar_map | letouzey |
| 2010-09-28 | Fix bug #2321, allowing "_" named projections in classes. Not realizing | msozeau |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2009-11-11 | Promote evar_defs to evar_map (in Evd) | glondu |
| 2009-10-28 | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
