aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Expand)AuthorAge
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Moving printing code from Evd to Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
| |\
| | * Fix a typo in STM universe communications.Gravatar Maxime Dénès2017-01-30
| * | 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-05
|\|
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\ \
| | * Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Gravatar Guillaume Melquiond2016-10-01
| |/
| * STM: compute the correct state for edited Qed (#5086)Gravatar Enrico Tassi2016-09-29
| * Cleanup API, making inference_hook optionalGravatar Matthieu Sozeau2016-09-29
| * Fix bug #4723 and FIXME in API for solve_by_tacGravatar Matthieu Sozeau2016-09-28
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
* | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\|
| * AsyncTaskQueue: annotate debug feedback messages with worker idGravatar Enrico Tassi2016-09-13
| * stm: feedback forwarding has to be atomicGravatar Enrico Tassi2016-09-13
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-07
|\ \ \ | | |/ | |/|
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-07
| |\ \
| * | | 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
| | * | Fix #5065: Anomaly: Not a proof by inductionGravatar Maxime Dénès2016-09-05
| * | | feedback: support multiple feedback listenersGravatar Enrico Tassi2016-09-05
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\| | |
| * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-02
| |\| |
| | * | Fix bug #5043: [Admitted] lemmas pick up section variables.Gravatar Pierre-Marie Pédrot2016-08-31
| | * | Fix #4871 - interrupting par:abstract kills coqtopGravatar Maxime Dénès2016-08-30
* | | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
|/ / /
| | * 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
| | * Unify location handling of error functions.Gravatar 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