index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
stm
Age
Commit message (
Expand
)
Author
2019-01-24
[STM] explicit handling of parsing states
Enrico Tassi
2019-01-24
Merge PR #9372: [thread] protect threads against sigalrm
Emilio Jesus Gallego Arias
2019-01-22
[thread] protect threads against sigalrm
Enrico Tassi
2019-01-22
Distinguish ASTs for Instance and Declare Instance
Maxime Dénès
2019-01-22
VernacDeclareClass -> VernacExistingClass
Maxime Dénès
2019-01-22
VernacDeclareInstances -> VernacExistingInstance
Maxime Dénès
2019-01-17
Merge PR #9326: [ci] compile with -quick & validate after vio2vo
Gaëtan Gilbert
2019-01-11
[STM] set the mtime of files generated via vio2vo (fix #9334)
Enrico Tassi
2019-01-11
Fix vernac classification of `Fail Instance`
Maxime Dénès
2019-01-10
[vio] free resources (file descriptors) as soon as a worker ends
Enrico Tassi
2019-01-10
[STM] kill no_safe_id anomaly
Enrico Tassi
2019-01-10
Merge PR #9331: [STM] Fix semantics of `cur_id` w.r.t. error states
Enrico Tassi
2019-01-09
[STM] Fix semantics of `cur_id` w.r.t. error states
Maxime Dénès
2019-01-09
Merge PR #9316: Fix #3934: coqc -time -quick gives unreadable output
Enrico Tassi
2019-01-08
Fix #3934: coqc -time -quick gives unreadable output
Maxime Dénès
2019-01-08
Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` p...
Maxime Dénès
2018-12-18
Merge PR #9218: [STM] Better protection for cur_id
Enrico Tassi
2018-12-17
[STM] Better protection for cur_id
Maxime Dénès
2018-12-17
Fix classification of Set Default Proof Mode.
Gaëtan Gilbert
2018-12-17
Merge PR #9206: [stm] join the tip of the document even when fixing a proof (...
Emilio Jesus Gallego Arias
2018-12-17
Merge PR #9219: [STM] Fix logic of debug DAG printer
Enrico Tassi
2018-12-17
Merge PR #9220: Move shallow state logic to the function preparing state for ...
Enrico Tassi
2018-12-14
[proof] Rework proof interface.
Emilio Jesus Gallego Arias
2018-12-13
[stm] join: check no error states are part of the document
Enrico Tassi
2018-12-13
[stm] join the tip of the document even when fixing a proof (fix #9204)
Enrico Tassi
2018-12-13
Move shallow state logic to the function preparing state for workers
Maxime Dénès
2018-12-13
[STM] Fix logic of debug DAG printer
Maxime Dénès
2018-12-12
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...
Maxime Dénès
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-12-06
Revise API for global universes.
Gaëtan Gilbert
2018-12-06
Fix race condition triggered by fresh universe generation
Maxime Dénès
2018-11-30
[vernac] [hooks] Refactor towards optional hooks.
Emilio Jesus Gallego Arias
2018-11-28
[options] New helper for creation of boolean options plus reference.
Emilio Jesus Gallego Arias
2018-11-27
Merge PR #9072: Clean stm flags
Enrico Tassi
2018-11-27
Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...
Emilio Jesus Gallego Arias
2018-11-27
Make `-async-proofs on` effective with `coqc`
Maxime Dénès
2018-11-27
Remove -async-proofs-full flag
Maxime Dénès
2018-11-23
change vernac_qed_type to have [VtKeep of vernac_keep_as]
Gaëtan Gilbert
2018-11-23
Local universes for opaque polymorphic constants.
Gaëtan Gilbert
2018-11-23
s/let _ =/let () =/ in some places (mostly goptions related)
Gaëtan Gilbert
2018-11-17
[vernacextend] Consolidate extension points API
Emilio Jesus Gallego Arias
2018-11-15
Move generating library dirpath to stm in compile mode.
Gaëtan Gilbert
2018-11-15
coqide: use correct toplevel name in files
Gaëtan Gilbert
2018-11-13
[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.
Emilio Jesus Gallego Arias
2018-11-05
Merge PR #8515: Command driven attributes
Pierre-Marie Pédrot
2018-11-02
Universe Polymorphism is a normal attribute modulo the stm (no Flags)
Gaëtan Gilbert
2018-11-02
Add comment in stm to unsupport attributes for special commands
Gaëtan Gilbert
2018-11-02
Make attributes more general to make defining #[universes(...)] easy
Gaëtan Gilbert
2018-11-02
Command driven attributes.
Gaëtan Gilbert
2018-11-02
{Vernacentries -> Attributes}.attributes_of_flags
Gaëtan Gilbert
[next]