aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.ml
AgeCommit message (Expand)Author
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
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-17[vernacextend] Consolidate extension points APIEmilio Jesus Gallego Arias
2018-11-15Move generating library dirpath to stm in compile mode.Gaëtan Gilbert
2018-11-15coqide: use correct toplevel name in filesGaëtan Gilbert
2018-11-05Merge PR #8515: Command driven attributesPierre-Marie Pédrot
2018-11-02Universe Polymorphism is a normal attribute modulo the stm (no Flags)Gaëtan Gilbert
2018-11-02Add comment in stm to unsupport attributes for special commandsGaëtan Gilbert
2018-10-30Move abstract out of tactics.mlGaëtan Gilbert
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-09-17Ensure_prev_proof returns a proof that has underlying differences fromJim Fehrle
2018-07-31Code to handle "Back" command for diffs.Jim Fehrle
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-06-18Remove reference name type.Maxime Dénès
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-05-17[STM] Nested Proofs Allowed has to be executed immediatelyEnrico Tassi
2018-05-17Remove deprecation warning for nested proofs.Théo Zimmermann
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-04-18Merge PR #7281: [stm] push functional API furtherEmilio Jesus Gallego Arias
2018-04-17[stm] push functional API furtherEnrico Tassi
2018-04-17[stm] expose restore/backup since ~doc is (still) dummyEnrico Tassi
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-11[warnings] Remove `set_current_loc` hack.Emilio Jesus Gallego Arias
2018-04-01[stm] More cleanup of "classification is not an interpreter"Emilio Jesus Gallego Arias
2018-04-01[stm] Move VernacBacktrack to the toplevel.Emilio Jesus Gallego Arias
2018-03-27stm: don't propagate side effects when editing a proofEnrico Tassi
2018-03-26Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer.Enrico Tassi
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
2018-03-11[stm] Never consider `Backtrack` as part of the script.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02[stm] Partial fix for bug #6884 [location missing from replay nodes]Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-15[toplevel] Make toplevel state into a record.Emilio Jesus Gallego Arias
2018-02-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
2018-02-06Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Maxime Dénès
2018-02-05Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve...Maxime Dénès
2018-02-05[stm] [toplevel] Make loadpath a parameter of the document.Emilio Jesus Gallego Arias
2018-02-01[vernac] Mutual theorems (VernacStartTheoremProof) always have namesVincent Laporte
2018-02-01[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 15:59:29 +0000