| Age | Commit message (Expand) | Author |
|---|
| 2016-05-08 | Removing dead code and unused opens. | Pierre-Marie Pédrot |
| 2016-03-20 | Pushing Proofview further down the dependency alley. | Pierre-Marie Pédrot |
| 2016-02-15 | merging conflicts with the original "trunk__CLEANUP__Context__2" branch | Matej Kosik |
| 2016-02-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-02-09 | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik |
| 2016-02-03 | More compact representation for evar resolvability flag. | Pierre-Marie Pédrot |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-11 | merge | Matej Kosik |
| 2016-01-11 | CLEANUP: kernel/context.ml{,i} | Matej Kosik |
| 2015-12-31 | Do not compose List.length with List.filter. | Guillaume Melquiond |
| 2015-12-05 | Moving extended_rel_vect/extended_rel_list to the kernel. | Hugo Herbelin |
| 2015-10-02 | Univs: fix many evar_map initializations and leaks. | Matthieu Sozeau |
| 2015-02-16 | Fix bug #3960: potential evar instance categorized as an unresolvable | Matthieu Sozeau |
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 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 |
