aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.ml
AgeCommit message (Expand)Author
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-13Removing a use of AUContext.instance in the STM.Pierre-Marie Pédrot
2017-07-13Safer API for Global.body_of_constant and variants.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-23Merge PR#821: [vernac] Remove stale bool parameter from `VernacStartTheoremPr...Maxime Dénès
2017-06-23Merge PR#815: STM: par: report no error to UIs in non-solve modeMaxime Dénès
2017-06-21[vernac] Remove stale bool parameter from `VernacStartTheoremProof`Emilio Jesus Gallego Arias
2017-06-20[stm] Fix route setting on VtQueryEmilio Jesus Gallego Arias
2017-06-20STM: par: report no error to UIs in non-solve modeEnrico Tassi
2017-06-18[ide] Add route_id parameter to query call.Emilio Jesus Gallego Arias
2017-06-15Merge PR#748: [stm] More fixes for nested commands [bugzilla 5589]Maxime Dénès
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-07[stm] More fixes for nested commands [bugzilla 5589]Emilio Jesus Gallego Arias
2017-06-07Merge PR#717: [proof] Deprecate "proof mode" APIMaxime Dénès
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-06Merge PR#716: Don't double up on periods in anomaliesMaxime Dénès
2017-06-03[stm] Solve bug 5577 "STM branch name is incorrect with Time"Emilio Jesus Gallego Arias
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-01[emacs] [toplevel] Make emacs flag local to the toplevel.Emilio Jesus Gallego Arias
2017-05-31[proof] Deprecate "proof mode" APIEmilio Jesus Gallego Arias
2017-05-27[stm] Rename Side-Effect type.Emilio Jesus Gallego Arias
2017-05-27[stm] Uniformize `Sideff / Sideff.Emilio Jesus Gallego Arias
2017-05-25Merge PR#645: [stm] Tweak debug options.Maxime Dénès
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-18[stm] Tweak debug options.Emilio Jesus Gallego Arias
2017-04-27Fix 4.04 warningsGaetan Gilbert
2017-04-27Remove unused constructorsGaetan Gilbert
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-12Merge PR#510: Correctly identify [Time Defined.] as a definedMaxime Dénès
2017-04-12Merge PR#441: Port Toplevel to the Stm APIMaxime Dénès
2017-04-12[toplevel] [stm] cleanup in module openEmilio Jesus Gallego Arias
2017-04-12[stm] [nit] Centralize compile-time debug flag.Emilio Jesus Gallego Arias
2017-04-12[stm] Improve error messages on add/parse.Emilio Jesus Gallego Arias
2017-04-12[stm] Port the toplevel to the STM.Emilio Jesus Gallego Arias
2017-04-12[stm] Move main parsing entry point to the STM.Emilio Jesus Gallego Arias
2017-04-12[stm] Remove edit_id.Emilio Jesus Gallego Arias
2017-04-07[stm] remove process_error_hookEmilio Jesus Gallego Arias
2017-04-07[stm] remove tactic_being_run hookEmilio Jesus Gallego Arias
2017-04-06Fix a few programming pearls related to Time, Fail and Redirect.Maxime Dénès
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-03-30Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-29Run non-tactic comands without resilient_commandTej Chajed
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24[stm] Remove some obsolete vernacs/classification.Emilio Jesus Gallego Arias
2017-03-23Correctly identify [Time Defined.] as a definedTej Chajed
2017-03-21[pp] Remove uses of expensive string_of_ppcmds.Emilio Jesus Gallego Arias