| Commit message (Expand) | Author | Age |
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey | 2016-07-03 |
* | Typeclasses:rename solve_instantiation* & use Hook | Matthieu Sozeau | 2016-06-16 |
* | Removing dead code and unused opens. | Pierre-Marie Pédrot | 2016-05-08 |
* | Pushing Proofview further down the dependency alley. | Pierre-Marie Pédrot | 2016-03-20 |
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branch | Matej Kosik | 2016-02-15 |
|\ |
|
* \ | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-02-13 |
|\ \ |
|
| | * | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik | 2016-02-09 |
| |/
|/| |
|
| * | More compact representation for evar resolvability flag. | Pierre-Marie Pédrot | 2016-02-03 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-21 |
|\| |
|
| * | Update copyright headers. | Maxime Dénès | 2016-01-20 |
* | | merge | Matej Kosik | 2016-01-11 |
|\ \ |
|
| * | | CLEANUP: kernel/context.ml{,i} | Matej Kosik | 2016-01-11 |
* | | | Do not compose List.length with List.filter. | Guillaume Melquiond | 2015-12-31 |
|/ / |
|
* / | Moving extended_rel_vect/extended_rel_list to the kernel. | Hugo Herbelin | 2015-12-05 |
|/ |
|
* | Univs: fix many evar_map initializations and leaks. | Matthieu Sozeau | 2015-10-02 |
* | Fix bug #3960: potential evar instance categorized as an unresolvable | Matthieu Sozeau | 2015-02-16 |
* | Removing dead code. | Pierre-Marie Pédrot | 2015-02-02 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evars | Hugo Herbelin | 2014-10-01 |
* | For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ... | Hugo Herbelin | 2014-09-18 |
* | Rework typeclass resolution and control of backtracking. | Matthieu Sozeau | 2014-09-15 |
* | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin | 2014-09-12 |
* | Add a flag for restricting resolution of typeclasses to | Matthieu Sozeau | 2014-09-11 |
* | instanciation is French, instantiation is English | Jason Gross | 2014-08-25 |
* | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau | 2014-08-03 |
* | Existing Class now works with universe polymorphism. Fixes HoTT bug #063 | Matthieu Sozeau | 2014-06-17 |
* | - 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 | 2014-05-06 |
* | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot | 2013-09-18 |
* | Optimizing some evar_maps manipulation. In particular, using a [map] instead | ppedrot | 2013-09-05 |
* | Actually using the domain function for maps. | ppedrot | 2013-08-25 |
* | Added printing of instance priority to the Print Instances command. | ppedrot | 2013-08-01 |
* | One more fix for rewrite: disallow resolving of the (partial) constraints | msozeau | 2013-06-12 |
* | 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-14 |
* | Use the Hook module here and there. | ppedrot | 2013-05-12 |
* | Merging Context and Sign. | ppedrot | 2013-04-29 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | code simplifications concerning Summary | letouzey | 2013-04-22 |
* | Finer fix for bug 3017, mark unresolvability only of goals that are | msozeau | 2013-04-18 |
* | Fix for bug #3017: wrong handling of the unresolvability status | msozeau | 2013-04-03 |
* | Fix bug# 2994, 2971 about better error messages. | msozeau | 2013-03-22 |
* | Restrict (try...with...) to avoid catching critical exn (part 12) | letouzey | 2013-03-13 |
* | Allowing different types of, not to be mixed, generic Stores through | ppedrot | 2013-03-12 |
* | Modulification of name | ppedrot | 2012-12-18 |
* | Finish patch for Hint Resolve, stopping to generate new constant names for | msozeau | 2012-12-08 |
* | Monomorphization (pretyping) | ppedrot | 2012-11-22 |