aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-12-18CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionMatej Kosik
2015-12-18CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Matej Kosik
2015-12-18CLEANUP: Vernacexpr.vernac_exprMatej Kosik
2015-12-04Specializing the Dyn module to each usecase.Pierre-Marie Pédrot
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-01vio: fix argument parsing (progress on #4442)Enrico Tassi
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-28Univs: correctly register universe binders for lemmas.Matthieu Sozeau
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-02Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico.Maxime Dénès
2015-11-02STM: fix undo into a branch containing side effectsEnrico Tassi
2015-11-02STM: never reopen a branch containing side effectsEnrico Tassi
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-30Add a way to get the right fix_exn in external vernacular commandsMatthieu Sozeau
2015-10-29Handle side-effects of Vernacular commands inside proofs better, so thatMatthieu Sozeau
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-18Miscellaneous typos, spacing, US spelling in comments or variable names.Hugo Herbelin
2015-10-17Clarifying and documenting the UState API.Pierre-Marie Pédrot
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14When typechecking a lemma statement, try to resolve typeclasses beforeMatthieu Sozeau
2015-10-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-09STM: Work around an occasional crash in dot (debug output)Alec Faithfull
2015-10-09TQueue: Allow some tasks to be saved when clearing a TQueueAlec Faithfull
2015-10-09TQueue: Expose the length of TQueuesAlec Faithfull
2015-10-09STM: Added functions for saving and restoring the internal stateAlec Faithfull
2015-10-09STM: Pass exception information to unreachable_state_hook functionsAlec Faithfull
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-08Axioms now support the universe binding syntax.Pierre-Marie Pédrot
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-10-08Spawn: use each socket exclusively for writing or readingEnrico Tassi
2015-10-08STM: for PIDE based UIs, edit_at requires no Reach.known_stateEnrico Tassi
2015-10-08STM: fix backtrace handlingEnrico Tassi
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: fix semantics of Type in proof mode in universe-polymorphic modeMatthieu Sozeau
2015-10-02Univs: fix handling of side effects/delayed proofsMatthieu Sozeau
2015-10-02Univs: fix many evar_map initializations and leaks.Matthieu Sozeau
2015-09-29Remove some uses of Loadpath.get_paths.Guillaume Melquiond
2015-09-26Hardening the API of evarmaps.Pierre-Marie Pédrot
2015-09-20Rich printing of messages.Pierre-Marie Pédrot
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-15STM: Reset takes Ltac <ident> into account (Close #4316)Enrico Tassi
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-09-08More potentialities in proof_terminators.Pierre-Marie Pédrot
2015-09-08Opacifying the proof_terminator type.Pierre-Marie Pédrot
2015-09-01STM: save a full state for queries.Enrico Tassi
2015-08-19Removing code duplication in Lemmas.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 11:38:26 +0000