index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
stm
Commit message (
Expand
)
Author
Age
*
CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified
Matej Kosik
2015-12-18
*
CLEANUP: Vernacexpr.VernacDeclareTacticDefinition
Matej Kosik
2015-12-18
*
CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...
Matej Kosik
2015-12-18
*
CLEANUP: Vernacexpr.vernac_expr
Matej Kosik
2015-12-18
*
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
[next]