aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2019-01-24[STM] explicit handling of parsing statesEnrico Tassi
2019-01-24Merge PR #9372: [thread] protect threads against sigalrmEmilio Jesus Gallego Arias
2019-01-22[thread] protect threads against sigalrmEnrico Tassi
2019-01-22Distinguish ASTs for Instance and Declare InstanceMaxime Dénès
2019-01-22VernacDeclareClass -> VernacExistingClassMaxime Dénès
2019-01-22VernacDeclareInstances -> VernacExistingInstanceMaxime Dénès
2019-01-17Merge PR #9326: [ci] compile with -quick & validate after vio2voGaëtan Gilbert
2019-01-11[STM] set the mtime of files generated via vio2vo (fix #9334)Enrico Tassi
2019-01-11Fix vernac classification of `Fail Instance`Maxime Dénès
2019-01-10[vio] free resources (file descriptors) as soon as a worker endsEnrico Tassi
2019-01-10[STM] kill no_safe_id anomalyEnrico Tassi
2019-01-10Merge PR #9331: [STM] Fix semantics of `cur_id` w.r.t. error statesEnrico Tassi
2019-01-09[STM] Fix semantics of `cur_id` w.r.t. error statesMaxime Dénès
2019-01-09Merge PR #9316: Fix #3934: coqc -time -quick gives unreadable outputEnrico Tassi
2019-01-08Fix #3934: coqc -time -quick gives unreadable outputMaxime Dénès
2019-01-08Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` p...Maxime Dénès
2018-12-18Merge PR #9218: [STM] Better protection for cur_idEnrico Tassi
2018-12-17[STM] Better protection for cur_idMaxime Dénès
2018-12-17Fix classification of Set Default Proof Mode.Gaëtan Gilbert
2018-12-17Merge PR #9206: [stm] join the tip of the document even when fixing a proof (...Emilio Jesus Gallego Arias
2018-12-17Merge PR #9219: [STM] Fix logic of debug DAG printerEnrico Tassi
2018-12-17Merge 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 documentEnrico Tassi
2018-12-13[stm] join the tip of the document even when fixing a proof (fix #9204)Enrico Tassi
2018-12-13Move shallow state logic to the function preparing state for workersMaxime Dénès
2018-12-13[STM] Fix logic of debug DAG printerMaxime Dénès
2018-12-12Merge 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-06Revise API for global universes.Gaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime 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-27Merge PR #9072: Clean stm flagsEnrico Tassi
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...Emilio Jesus Gallego Arias
2018-11-27Make `-async-proofs on` effective with `coqc`Maxime Dénès
2018-11-27Remove -async-proofs-full flagMaxime Dénès
2018-11-23change vernac_qed_type to have [VtKeep of vernac_keep_as]Gaëtan Gilbert
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-17[vernacextend] Consolidate extension points APIEmilio Jesus Gallego Arias
2018-11-15Move generating library dirpath to stm in compile mode.Gaëtan Gilbert
2018-11-15coqide: use correct toplevel name in filesGaëtan Gilbert
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias
2018-11-05Merge PR #8515: Command driven attributesPierre-Marie Pédrot
2018-11-02Universe Polymorphism is a normal attribute modulo the stm (no Flags)Gaëtan Gilbert
2018-11-02Add comment in stm to unsupport attributes for special commandsGaëtan Gilbert
2018-11-02Make attributes more general to make defining #[universes(...)] easyGaëtan Gilbert
2018-11-02Command driven attributes.Gaëtan Gilbert
2018-11-02{Vernacentries -> Attributes}.attributes_of_flagsGaëtan Gilbert