| Age | Commit message (Expand) | Author |
|---|
| 2014-10-01 | Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evars | Hugo Herbelin |
| 2014-09-18 | For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ... | Hugo Herbelin |
| 2014-09-15 | Rework typeclass resolution and control of backtracking. | Matthieu Sozeau |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin |
| 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-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-06-17 | Existing Class now works with universe polymorphism. Fixes HoTT bug #063 | Matthieu Sozeau |
| 2014-05-06 | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau |
| 2014-05-06 | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau |
| 2014-05-06 | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-09-05 | Optimizing some evar_maps manipulation. In particular, using a [map] instead | ppedrot |
| 2013-08-25 | Actually using the domain function for maps. | ppedrot |
| 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-14 | Delayed the computation of parameters in sort polymorphism of | herbelin |
| 2013-05-14 | Replacing compatibility layer for Fmap in Typeclasses. Code was | ppedrot |
| 2013-05-14 | More semantical-friendly function. | ppedrot |
| 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-22 | code simplifications concerning Summary | letouzey |
| 2013-04-18 | Finer fix for bug 3017, mark unresolvability only of goals that are | msozeau |
| 2013-04-03 | Fix for bug #3017: wrong handling of the unresolvability status | msozeau |
| 2013-03-22 | Fix bug# 2994, 2971 about better error messages. | msozeau |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 12) | letouzey |
| 2013-03-12 | Allowing different types of, not to be mixed, generic Stores through | ppedrot |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-08 | Finish patch for Hint Resolve, stopping to generate new constant names for | msozeau |
| 2012-11-22 | Monomorphization (pretyping) | ppedrot |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-04 | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau |
| 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-18 | Fix for subclasses implementation, allowing to register generalized classes s... | msozeau |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-11-02 | Add type annotations around all calls to Libobject.declare_object | letouzey |
| 2011-10-07 | Fix bug #2557 and an issue with Propers for complement | msozeau |
| 2011-04-13 | - Make typeclass transparency information directly available | msozeau |
