aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.ml
AgeCommit message (Expand)Author
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-09[stm] move par: implementation to vernac/comTactic and stm/partacEnrico Tassi
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-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-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-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-19[obligations] More progress towards unification of the save pathEmilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-04Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.Pierre-Marie Pédrot
2020-03-03[stm] Port documentation of init options to ocamldocEmilio Jesus Gallego Arias
2020-03-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-28Merge PR #11609: [stm] Use Default Proof Using only with ProofEnrico Tassi
2020-02-28[stm] Use Default Proof Using only with ProofTej Chajed
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio Jesus Gallego Arias
2020-02-13Merge PR #11564: Recognize Default Proof Using in STMEnrico Tassi
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-10Recognize Default Proof Using in STMTej Chajed
2020-01-27cleanup: Lib.freeze doesn't use its [~marshallable] argumentGaëtan Gilbert
2019-11-08Make [Proof_global.closed_proof_output] opaqueGaëtan Gilbert
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-11-01Implementing support for vos/vok files.charguer
2019-10-12Merge PR #10818: Merge Direct and Indirect nodes in Opaqueproof.Maxime Dénès
2019-10-07[vernac] Split vernacular translation and interpretation.Emilio Jesus Gallego Arias
2019-10-04Merge Direct and Indirect nodes in Opaqueproof.Pierre-Marie Pédrot
2019-09-09Merge PR #10605: [toplevel] Make all argument lists to be in user-declared or...Hugo Herbelin
2019-08-14[vernac] Refactor common parts of interp_{,delayed}Emilio Jesus Gallego Arias
2019-08-14[vernac] Pass control attributes to interpretation of delayed proofs.Emilio Jesus Gallego Arias
2019-08-14[vernac] Refactor Vernacular Control Attributes into a listEmilio Jesus Gallego Arias
2019-07-31[toplevel] Make all argument lists to be in user-declared order.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:04:30 +0000