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
*
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
|
|
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
|
/
/
|
/
|
|
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
|
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
|
*
|
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Maxime Dénès
2016-01-15
*
|
|
CLEANUP: removing unnecessary wrapper
Matej Kosik
2016-01-11
*
|
|
CLEANUP: removing unused field
Matej Kosik
2016-01-11
*
|
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Guillaume Melquiond
2016-01-05
|
\
|
|
|
*
|
fixup d2b468a, evar normalization is needed
Enrico Tassi
2016-01-04
|
*
|
par: check if the goal is not ground and fail (fix #4465)
Enrico Tassi
2016-01-04
|
*
|
workers: purge short version of -load-vernac too (fix #4458)
Enrico Tassi
2016-01-04
*
|
|
Remove some unused functions.
Guillaume Melquiond
2016-01-02
*
|
|
Remove some useless module opening.
Guillaume Melquiond
2016-01-02
*
|
|
Reduce dependencies of interface files.
Guillaume Melquiond
2016-01-02
*
|
|
Remove unused functions.
Guillaume Melquiond
2016-01-01
[next]