aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.ml
Commit message (Expand)AuthorAge
* [stm] Move main parsing entry point to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [stm] remove process_error_hookGravatar Emilio Jesus Gallego Arias2017-04-07
* [stm] remove tactic_being_run hookGravatar Emilio Jesus Gallego Arias2017-04-07
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-30
|\
| * Run non-tactic comands without resilient_commandGravatar Tej Chajed2017-03-29
* | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
* | [pp] Remove uses of expensive string_of_ppcmds.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | [pp] [ide] Minor cleanups in pp code.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | [future] Remove unused parameter greedy.Gravatar Emilio Jesus Gallego Arias2017-03-14
* | Make Obligations see fix_exnGravatar Enrico Tassi2017-02-15
* | [stm] Remove unused legacy stm interface.Gravatar Emilio Jesus Gallego Arias2017-02-15
* | [stm] Reenable Show Script command.Gravatar Emilio Jesus Gallego Arias2017-02-15
* | [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\|
| * STM: fix run-time classification of VernacInstance (fix #5313)Gravatar Enrico Tassi2017-01-17
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\|
| * STM: cur_id must be invalid if an error occurs (fix #5191)Gravatar Enrico Tassi2016-11-29
| * Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
| * [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * STM: make ~valid state id non optional from APIsGravatar Enrico Tassi2016-10-26
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\|
| * [stm] Fix record field name clash.Gravatar Emilio Jesus Gallego Arias2016-10-18
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * STM: compute the correct state for edited Qed (#5086)Gravatar Enrico Tassi2016-09-29
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\|
| * stm: feedback forwarding has to be atomicGravatar Enrico Tassi2016-09-13
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ | |/ |/|
* | STM: if_verbose on "Checking task ..." (fix #4058)Gravatar Enrico Tassi2016-09-07
* | STM: queries give back a dummy safe_id in case of error (#5041)Gravatar Enrico Tassi2016-09-06
* | STM: sideff: report safe_id correctly (fix #4968)Gravatar Enrico Tassi2016-09-06
* | STM: nested Abort is like nested Qed (fix #4756)Gravatar Enrico Tassi2016-09-06
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* [feedback] Remove `ErrorMsg` in favor of `Message Error`.Gravatar Emilio Jesus Gallego Arias2016-06-25
* par: like all: but in parallelGravatar Enrico Tassi2016-06-17
* Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\
* \ Merge remote-tracking branch 'origin/pr/205' into trunkGravatar Enrico Tassi2016-06-14
|\ \
* \ \ Merge remote-tracking branch 'origin/pr/182' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \
| | * | STM classification: VernacTimeout may contain an "internal command".Gravatar Maxime Dénès2016-06-13
| | * | Print Assumptions and co. can "pierce opacity".Gravatar Maxime Dénès2016-06-13
* | | | DocumentationGravatar Enrico Tassi2016-06-07
* | | | Renaming: ErrorBlock -> ProofBlockGravatar Enrico Tassi2016-06-06
* | | | STM: each proof block can be enabled separatelyGravatar Enrico Tassi2016-06-06
* | | | Error box detection run only on errorGravatar Enrico Tassi2016-06-06
* | | | rebase on trunkGravatar Enrico Tassi2016-06-06