aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.ml
AgeCommit message (Expand)Author
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-27Remove the delayed universe table from object files.Pierre-Marie Pédrot
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
2019-05-24Merge PR #10209: Fix #10208 don't fail when passed extensionless -topfileEnrico Tassi
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-05-24Statically ensure the content of delayed proofs in vio file.Pierre-Marie Pédrot
2019-05-24Remove a useless call to the Future API for opaque proofs in the STM.Pierre-Marie Pédrot
2019-05-23Fixing typos - Part 3JPR
2019-05-23Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ...Maxime Dénès
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
2019-05-22unified style for new hooks and old hooksTalia Ringer
2019-05-22Merge remote-tracking branch 'origin/master' into stm+doc_hookTalia Ringer
2019-05-22Fix #10208 don't fail when passed extensionless -topfileGaëtan Gilbert
2019-05-21[loadpath] Make loadpath handling self-contained and move to vernacEmilio Jesus Gallego Arias
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
2019-05-20Remove VtUnknown classificationMaxime Dénès
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
2019-05-04Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.Pierre-Marie Pédrot
2019-04-29[stm] Add hooks for document actions.Emilio Jesus Gallego Arias
2019-04-29Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is ...Maxime Dénès
2019-04-25[vernac] [ast] Make location info an attribute of vernaculars.Emilio Jesus Gallego Arias
2019-04-11[stm] Report correct ids on some errors where it was dummy.Shachar Itzhaky
2019-04-09[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.Emilio Jesus Gallego Arias
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-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-05[parsing] Use AST node for main parsing entry.Emilio Jesus Gallego Arias
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.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-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-17[STM] Better protection for cur_idMaxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 00:08:20 +0000