aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
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-14Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive Para...Maxime Dénès
2020-02-13Merge PR #11564: Recognize Default Proof Using in STMEnrico Tassi
2020-02-13Don't duplicate the inductive keyword for each block elt when parsingGaëtan Gilbert
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-10Recognize Default Proof Using in STMTej Chajed
2020-01-29[rfc] [mltop] Removal of dynamic loading of object and `.ml` filesEmilio Jesus Gallego Arias
2020-01-27cleanup: Lib.freeze doesn't use its [~marshallable] argumentGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-13Return of Refine Instance as an attribute.Gaë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-26[glob/aux files] Remove undocumented Stdout dump, cleanup flags.Emilio Jesus Gallego Arias
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
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
2019-07-23[vernacexpr] Remove duplicate fixpoint record.Emilio Jesus Gallego Arias
2019-07-23[vernacexpr] Refactor fixpoint AST.Emilio Jesus Gallego Arias
2019-07-11Remove Stm.call_process_error_onceGaëtan Gilbert
2019-07-08Merge PR #9686: [error] Remove special error printing pre-processingGaëtan Gilbert
2019-07-08Passing command-line option async_proofs_worker_priority functionally.Hugo Herbelin
2019-07-08Layout/documentation updates.Hugo Herbelin
2019-07-08An attempt to reorganize further coqtop initialization into semantic units.Hugo Herbelin
2019-07-07[error] Remove special error printing pre-processingEmilio Jesus Gallego Arias
2019-07-03Merge PR #10338: Fix #9455: avoid update_global_env when unchanged Global.uni...Emilio Jesus Gallego Arias
2019-06-30Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG.Emilio Jesus Gallego Arias
2019-06-26[stm] [vernac] Remove special ?proof parameter from vernac main pathEmilio Jesus Gallego Arias
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
2019-06-25[lemmas] Move `Stack` out of Lemmas.Emilio Jesus Gallego Arias
2019-06-24[proof] API Documentation fixes.Emilio Jesus Gallego Arias
2019-06-24[api] [proof] Move `discharge` type to vernac_ast where it is used.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Turn Lemmas.info into a proper type with constructor.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Reify info for implicits, univ_decls, prepare for rec_thms.Emilio Jesus Gallego Arias
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...Pierre-Marie Pédrot
2019-06-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:39:33 +0000