aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2019-04-05Merge PR #9685: [vernac] Small cleanup to remove assert false.Vincent Laporte
2019-04-03Protect some I/O routines from SIGALRMMaxime Dénès
2019-03-30[vernac] Small cleanup to remove assert false.Emilio Jesus Gallego Arias
2019-03-27[vernac] [stm] Tweak `with_fail` and hopefully fix the semantics.Emilio Jesus Gallego Arias
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-25[Vernacular] Deprecate the “Show Script” commandVincent Laporte
2019-03-04[stm] unfocus when edition exits the proof (fix #9431)Enrico Tassi
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:35:06 +0000