aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2021-04-14Remove remote counter systemGaëtan Gilbert
2021-04-09Make critical sections safe in the presence of exceptionsLasse Blaauwbroek
2021-03-23Do not match on record types with mutable fields in function arguments.Guillaume Melquiond
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-01-27make the linter happyEnrico Tassi
2021-01-27[sysinit] move initialization code from coqtop to hereEnrico Tassi
2021-01-27[sysinit] new component for system initializationEnrico Tassi
2021-01-27[vernac] move vernac_classifier to vernacEnrico Tassi
2021-01-27[ltac] break dependency on the STMEnrico Tassi
2021-01-26[options] improve support for appendEnrico Tassi
2021-01-13Avoid using "subgoals" in the UI, it means the same as "goals"Jim Fehrle
2020-12-03[coqide] fix procedure to parse argumentsEnrico Tassi
2020-11-27Improved error message on nested proofsFabian Kunze
2020-11-20[stm] [declare] Remove pinfo internals hack.Emilio Jesus Gallego Arias
2020-11-20[stm] [declare] Try to propagate safe bits of proof informationEmilio Jesus Gallego Arias
2020-11-02[stm] support #[using] attributeEnrico Tassi
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
2020-10-09[stm] move par: implementation to vernac/comTactic and stm/partacEnrico Tassi
2020-09-01Unify the shelvesMaxime Dénès
2020-08-31Update update_global_env usageGaëtan Gilbert
2020-08-28par: print relevant subgoal when failingGaëtan Gilbert
2020-08-27[state] A few nits after consolidation of state.Emilio Jesus Gallego Arias
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
2020-06-26[declare] Improve logical code orderEmilio Jesus Gallego Arias
2020-06-26[declare] Improve organization of proof/constant information.Emilio Jesus Gallego Arias
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
2020-06-23Fix #4459 by improving `par:` error messageMaxime Dénès
2020-06-11[stm] Simplify logic involving forced futures.Emilio Jesus Gallego Arias
2020-06-11[declare] Remove some unused `fix_exn`Emilio Jesus Gallego Arias
2020-05-26Fix worker handling of command-line options that are already included in init...Théo Zimmermann
2020-05-26Remove command-line options that do not exist anymore.Théo Zimmermann
2020-05-18[declare] Grand unification of the proof save path.Emilio Jesus Gallego Arias
2020-05-18[declare] Merge `DeclareObl` into `Declare`Emilio Jesus Gallego Arias
2020-05-18[obligations] Pre-functionalize Program stateEmilio Jesus Gallego Arias
2020-05-12Interleave commandline require/set/unset commandsLasse Blaauwbroek
2020-05-03Remove a very specific low-level tactical from Refiner.Pierre-Marie Pédrot
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-02Fix options listed in asycTaskQueue.Théo Zimmermann
2020-03-31[proof] [stm] Force `opaque` in `close_future_proof`Emilio Jesus Gallego Arias
2020-03-31[proof] Split return_proof in partial and regular versions.Emilio Jesus Gallego Arias
2020-03-31[proof] Split delayed and regular proof closing functions, part IIEmilio Jesus Gallego Arias
2020-03-22Merge PR #11731: [proof] Miscellaneous refactoringsGaëtan Gilbert
2020-03-19[obligations] More progress towards unification of the save pathEmilio Jesus Gallego Arias
2020-03-19Make Cumulative, NonCumulative and Private attributes.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 06:43:28 +0000