aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2019-02-08Merge PR #9525: Remove global output_native_objects flag.Emilio Jesus Gallego Arias
2019-02-08Merge PR #9523: Make boot flag into a normal option (no global flag).Emilio Jesus Gallego Arias
2019-02-08Merge PR #9481: [parsing] Use AST node for main parsing entry.Enrico Tassi
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-08Make boot flag into a normal option (no global flag).Gaëtan Gilbert
2019-02-08[stm] Filter some more arguments that shouldn't be sent to workers.Emilio Jesus Gallego Arias
2019-02-05[parsing] Use AST node for main parsing entry.Emilio Jesus Gallego Arias
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Primitive integersMaxime Dénès
2019-02-01[toplevel] Split interactive toplevel and compiler binaries.Emilio Jesus Gallego Arias
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2019-01-28[vernac] Fix classification of `Declare Custom Entry`Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 00:15:04 +0000