| Age | Commit message (Expand) | Author |
|---|
| 2015-12-21 | Using dynamic values in tactic evaluation. | Pierre-Marie Pédrot |
| 2015-12-17 | CLEANUP: in the Reduction module | Matej Kosik |
| 2015-12-17 | CLEANUP: in the Reductionops module | Matej Kosik |
| 2015-12-17 | CLEANUP: in the Reduction module | Matej Kosik |
| 2015-12-15 | Fixing unexpected length of context in a typing function, detected by | Hugo Herbelin |
| 2015-12-15 | Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite. | Hugo Herbelin |
| 2015-12-15 | API: documenting context_chop and removing a duplicate. | Hugo Herbelin |
| 2015-12-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-12-11 | Optimize occur_evar_upto_types, avoiding repeateadly looking into the | Matthieu Sozeau |
| 2015-12-05 | Unifying betazeta_applist and prod_applist into a clearer interface. | Hugo Herbelin |
| 2015-12-05 | Moving extended_rel_vect/extended_rel_list to the kernel. | Hugo Herbelin |
| 2015-12-05 | Simplifying an instantiation function using subst_of_rel_context_instance. | Hugo Herbelin |
| 2015-12-05 | About building of substitutions from instances. | Hugo Herbelin |
| 2015-12-05 | An example in centralizing similar functions to a common place so that | Hugo Herbelin |
| 2015-12-04 | Removing dynamic inclusion of constrs in tactic AST. | Pierre-Marie Pédrot |
| 2015-12-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-12-02 | Add an option to deactivate compatibility printing of primitive | Matthieu Sozeau |
| 2015-11-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-11-27 | Univs: entirely disallow instantiation of polymorphic constants with | Matthieu Sozeau |
| 2015-11-26 | More efficient implementation of equality-up-to-universes in Universes. | Pierre-Marie Pédrot |
| 2015-11-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-11-25 | Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej). | Hugo Herbelin |
| 2015-11-24 | Fixing an old typo in Retyping, found by Matej. | Hugo Herbelin |
| 2015-11-22 | Fixing a vm_compute bug in the presence of let-ins among the | Hugo Herbelin |
| 2015-11-22 | Fixing a bug of adjust_subst_to_rel_context. | Hugo Herbelin |
| 2015-11-22 | Fixing kernel bug in typing match with let-ins in the arity. | Hugo Herbelin |
| 2015-11-20 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-11-19 | Fix bug #4433, removing hack on evars appearing in a pattern from a | Matthieu Sozeau |
| 2015-11-17 | Performance fix for destruct. | Pierre-Marie Pédrot |
| 2015-11-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-11-11 | Ensure that conversion is called on terms of the same type in | Matthieu Sozeau |
| 2015-11-11 | Fix bug #3998: when using typeclass resolution for conversion, allow | Matthieu Sozeau |
| 2015-11-11 | Fix bug #4293: ensure let-ins do not contain algebraic universes in | Matthieu Sozeau |
| 2015-11-10 | Revert "Fixing #1225: we now skip the canonically built binding contexts of" | Hugo Herbelin |
| 2015-11-10 | Fixing #1225: we now skip the canonically built binding contexts of | Hugo Herbelin |
| 2015-11-10 | Merge origin/v8.5 into trunk | Hugo Herbelin |
| 2015-11-09 | Pushing the backtrace in conversion anomalies. | Pierre-Marie Pédrot |
| 2015-11-07 | Experimenting printing the type of the defined term of a LetIn when | Hugo Herbelin |
| 2015-11-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-11-04 | Univs: missing checks in evarsolve with candidates and missing a | Matthieu Sozeau |
| 2015-11-04 | Univs: update refman, better printers for universe contexts. | Matthieu Sozeau |
| 2015-11-04 | Univs: compatibility with 8.4. | Matthieu Sozeau |
| 2015-11-02 | Fix bug #4151: discrepancy between exact and eexact/eassumption. | Matthieu Sozeau |
| 2015-11-02 | Refresh rigid universes as well, and in 8.4 compatibility mode, | Matthieu Sozeau |
| 2015-10-29 | Handle side-effects of Vernacular commands inside proofs better, so that | Matthieu Sozeau |
| 2015-10-29 | Removing some goal unsafeness in inductive schemes. | Pierre-Marie Pédrot |
| 2015-10-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-28 | Univs: local names handling. | Matthieu Sozeau |
| 2015-10-28 | Avoid type checking private_constants (side_eff) again during Qed (#4357). | Enrico Tassi |
| 2015-10-28 | Fix bug in native compiler with universe polymorphism. | Maxime Dénès |
