| Commit message (Expand) | Author | Age |
* | Specializing the Dyn module to each usecase. | Pierre-Marie Pédrot | 2015-12-04 |
* | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-12-03 |
|\ |
|
| * | vio: fix argument parsing (progress on #4442) | Enrico Tassi | 2015-12-01 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-11-29 |
|\| |
|
| * | Univs: correctly register universe binders for lemmas. | Matthieu Sozeau | 2015-11-28 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-11-05 |
|\| |
|
| * | Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico. | Maxime Dénès | 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-11-02 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-30 |
|\| |
|
| * | Add a way to get the right fix_exn in external vernacular commands | Matthieu Sozeau | 2015-10-30 |
| * | Handle side-effects of Vernacular commands inside proofs better, so that | Matthieu Sozeau | 2015-10-29 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-29 |
|\| |
|
| * | Avoid type checking private_constants (side_eff) again during Qed (#4357). | Enrico Tassi | 2015-10-28 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-19 |
|\| |
|
| * | Miscellaneous typos, spacing, US spelling in comments or variable names. | Hugo Herbelin | 2015-10-18 |
* | | Clarifying and documenting the UState API. | Pierre-Marie Pédrot | 2015-10-17 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-15 |
|\| |
|
| * | When typechecking a lemma statement, try to resolve typeclasses before | Matthieu Sozeau | 2015-10-14 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-10 |
|\| |
|
| * | STM: Work around an occasional crash in dot (debug output) | Alec Faithfull | 2015-10-09 |
| * | TQueue: Allow some tasks to be saved when clearing a TQueue | Alec Faithfull | 2015-10-09 |
| * | TQueue: Expose the length of TQueues | Alec Faithfull | 2015-10-09 |
| * | STM: Added functions for saving and restoring the internal state | Alec Faithfull | 2015-10-09 |
| * | STM: Pass exception information to unreachable_state_hook functions | Alec Faithfull | 2015-10-09 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-09 |
|\| |
|
| * | Axioms now support the universe binding syntax. | Pierre-Marie Pédrot | 2015-10-08 |
| * | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi | 2015-10-08 |
| * | Spawn: use each socket exclusively for writing or reading | Enrico Tassi | 2015-10-08 |
| * | STM: for PIDE based UIs, edit_at requires no Reach.known_state | Enrico Tassi | 2015-10-08 |
| * | STM: fix backtrace handling | Enrico Tassi | 2015-10-08 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-02 |
|\| |
|
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-10-02 |
|\ \ |
|
| | * | Univs: fix semantics of Type in proof mode in universe-polymorphic mode | Matthieu Sozeau | 2015-10-02 |
| | * | Univs: fix handling of side effects/delayed proofs | Matthieu Sozeau | 2015-10-02 |
| | * | Univs: fix many evar_map initializations and leaks. | Matthieu Sozeau | 2015-10-02 |
| |/ |
|
| * | Remove some uses of Loadpath.get_paths. | Guillaume Melquiond | 2015-09-29 |
* | | Hardening the API of evarmaps. | Pierre-Marie Pédrot | 2015-09-26 |
* | | Rich printing of messages. | Pierre-Marie Pédrot | 2015-09-20 |
* | | Merge branch 'v8.5' into trunk | Maxime Dénès | 2015-09-17 |
|\| |
|
| * | STM: Reset takes Ltac <ident> into account (Close #4316) | Enrico Tassi | 2015-09-15 |
| * | Univs: Add universe binding lists to definitions | Matthieu Sozeau | 2015-09-14 |
* | | More potentialities in proof_terminators. | Pierre-Marie Pédrot | 2015-09-08 |
* | | Opacifying the proof_terminator type. | Pierre-Marie Pédrot | 2015-09-08 |
|/ |
|
* | STM: save a full state for queries. | Enrico Tassi | 2015-09-01 |
* | Removing code duplication in Lemmas. | Pierre-Marie Pédrot | 2015-08-19 |
* | Documentation by giving a name to a large type. | Pierre-Marie Pédrot | 2015-08-19 |
* | STM: make multiple, admitted, nested proofs work (fix #4314) | Enrico Tassi | 2015-07-30 |
* | STM: emit a warning when a QED/Admitted proof contains a nested lemma | Enrico Tassi | 2015-07-30 |
* | STM: fix backtrack in presence of nested, immediate, proofs | Enrico Tassi | 2015-07-30 |