| Age | Commit message (Expand) | Author |
|---|
| 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 | Hint Cut documentation and cleanup of printing (was duplicated and | Matthieu Sozeau |
| 2015-11-04 | Univs: compatibility with 8.4. | Matthieu Sozeau |
| 2015-11-04 | Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion | Matthieu Sozeau |
| 2015-11-04 | Test file for #4397. | Maxime Dénès |
| 2015-11-03 | Update compatibility file for some of bug #4392 | Jason Gross |
| 2015-11-02 | Fix bug #4397: refreshing types in abstract_generalize. | 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-11-02 | Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico. | Maxime Dénès |
| 2015-11-02 | Adding syntax "Show id" to show goal named id (shelved or not). | Hugo Herbelin |
| 2015-11-02 | Made that the syntax [id]:tac also applies to the shelve, which is after all ... | Hugo Herbelin |
| 2015-11-02 | STM: fix undo into a branch containing side effects | Enrico Tassi |
| 2015-11-02 | STM: never reopen a branch containing side effects | Enrico Tassi |
| 2015-10-30 | Command.declare_definition: grab the fix_exn early (follows 77cf18e) | Enrico Tassi |
| 2015-10-30 | Manually expand red_tactic so that notations do not break reduction tactics. ... | Guillaume Melquiond |
| 2015-10-30 | Add a way to get the right fix_exn in external vernacular commands | Matthieu Sozeau |
| 2015-10-30 | Fix typo. | Guillaume Melquiond |
| 2015-10-29 | Handle side-effects of Vernacular commands inside proofs better, so that | Matthieu Sozeau |
| 2015-10-29 | Collect subproof universes in handle_side_effects. | Matthieu Sozeau |
| 2015-10-29 | Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392) | Guillaume Melquiond |
| 2015-10-29 | Avoid an anomaly when destructing an unknown ident. (Fix bug #4395) | Guillaume Melquiond |
| 2015-10-29 | Fixing another instance of bug #3267 in eauto, this time in the | Hugo Herbelin |
| 2015-10-29 | Cleanup API and comments of 908dcd613 | Enrico Tassi |
| 2015-10-29 | Accept option -compat 8.5. (Fix bug #4393) | Guillaume Melquiond |
| 2015-10-28 | Univs: local names handling. | Matthieu Sozeau |
| 2015-10-28 | Printing of @{} instances for polymorphic references in Print and About. | Matthieu Sozeau |
| 2015-10-28 | Avoid type checking private_constants (side_eff) again during Qed (#4357). | Enrico Tassi |
| 2015-10-28 | lib_stack: API to reorder the libstack | Enrico Tassi |
| 2015-10-28 | Fix test suite after Matthieu's ed7af646f2e486b. | Maxime Dénès |
| 2015-10-28 | Fix bug in native compiler with universe polymorphism. | Maxime Dénès |
| 2015-10-28 | Refine Gregory Malecha's patch on VM and universe polymorphism. | Maxime Dénès |
| 2015-10-28 | Conversion of polymorphic inductive types was incomplete in VM and native. | Maxime Dénès |
| 2015-10-28 | Fix minor typo in native compiler. | Maxime Dénès |
| 2015-10-28 | test cases. | Gregory Malecha |
| 2015-10-28 | Adds support for the virtual machine to perform reduction of universe polymor... | Gregory Malecha |
| 2015-10-28 | Univs: fix bug #4375, accept universe binders on (co)-fixpoints | Matthieu Sozeau |
| 2015-10-28 | Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins" | Hugo Herbelin |
| 2015-10-28 | Seeing configure as a static resolution of path continued (not yet on windows). | Hugo Herbelin |
| 2015-10-28 | Do not pause globing in funind. (Fix bug #4382) | Guillaume Melquiond |
| 2015-10-27 | Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names | Matthieu Sozeau |
| 2015-10-26 | Seeing configure as a static resolution of path, hence hardwiring long | Hugo Herbelin |
| 2015-10-26 | Fixing bugs in options of the configure. | Hugo Herbelin |
| 2015-10-26 | Preventing using OCaml 4.02.0 for compiling Coq as compilation times | Hugo Herbelin |
| 2015-10-26 | Documenting a bit more interpretation functions in passing. | Hugo Herbelin |
| 2015-10-26 | Preserving goal name in revert/bring_hyps. | Hugo Herbelin |
| 2015-10-26 | Two test-suite files for bugs 3974 and 3975 | Pierre Letouzey |
| 2015-10-25 | Declaremods: replace two anomalies by user errors (fix #3974 and #3975) | Pierre Letouzey |
| 2015-10-25 | Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331) | Pierre Letouzey |
