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
*
Documentation
Enrico Tassi
2016-06-07
*
Renaming: ErrorBlock -> ProofBlock
Enrico Tassi
2016-06-06
*
STM: each proof block can be enabled separately
Enrico Tassi
2016-06-06
*
Error box detection run only on error
Enrico Tassi
2016-06-06
*
STM: proof block detection for indentation
Enrico Tassi
2016-06-06
*
rebase on trunk
Enrico Tassi
2016-06-06
*
STM: fix error reporting of par:
Enrico Tassi
2016-06-06
*
STM: proof block detection made optional + simple test
Enrico Tassi
2016-06-06
*
STM: proof block detection for par:
Enrico Tassi
2016-06-06
*
STM: proof block detection for bullets and { block }
Enrico Tassi
2016-06-06
*
STM: proof block detection/error resilience API
Enrico Tassi
2016-06-06
*
STM: carry AST and indentation of document commands
Enrico Tassi
2016-06-06
*
STM: support for nested boxes of nodes to model error boundaries
Enrico Tassi
2016-06-06
*
STM: invalid states are first class citizens
Enrico Tassi
2016-06-06
*
Move serialization functions out of Stm
Emilio Jesus Gallego Arias
2016-06-02
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-01
|
\
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
*
STM: fix argument filtering for slaves
Enrico Tassi
2016-05-27
|
*
Pfedit.get_current_context refinement (fix #4523)
Matthieu Sozeau
2016-05-26
*
|
typos
Enrico Tassi
2016-05-23
*
|
Put the "cofix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
Put the "fix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"
Enrico Tassi
2016-05-10
*
|
STM: code cleanup
Enrico Tassi
2016-05-10
*
|
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
|
*
Fix for #4603, part 3: definitions inside proofs not handled properly by coqc.
Maxime Dénès
2016-05-04
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-24
|
\
|
|
*
Build stm debugging messages lazily so that they are not silently
Hugo Herbelin
2016-04-15
|
*
Quick fix for #4603 (part 2): Anomaly: Universe undefined
Maxime Dénès
2016-04-12
*
|
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
\
*
\
\
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-30
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Univs: fix get_current_context (bug #4603, part I)
Matthieu Sozeau
2016-03-25
*
|
|
Moving the Ltac definition command to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Moving Tactic Notation to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Moving VernacSolve to an EXTEND-based definition.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Removing the dependency in VernacSolve in the STM.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Relying on Vernac classifier to flag tactics in the STM.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-18
|
\
|
|
|
*
|
Tentative fix for bug #4614: "Fully check the document" is uninterruptable.
Pierre-Marie Pédrot
2016-03-15
*
|
|
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Hugo Herbelin
2016-03-13
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
|
|
*
|
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-21
|
\
|
|
|
*
|
STM: Print/Extraction have to be skipped if -quick
Enrico Tassi
2016-02-19
|
*
|
STM: classify some variants of Instance as regular `Fork nodes.
Enrico Tassi
2016-02-19
*
|
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
\
*
\
\
\
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-13
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
|
*
|
|
STM: always stock in vio files the first node (state) of a proof
Enrico Tassi
2016-02-10
|
*
|
|
STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530
Enrico Tassi
2016-02-10
[next]