aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Expand)AuthorAge
* 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.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
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* | Univs: earlier errors for strict univ decls #4527Gravatar Matthieu Sozeau2016-06-29
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\|
* | [feedback] Remove `ErrorMsg` in favor of `Message Error`.Gravatar Emilio Jesus Gallego Arias2016-06-25
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* | par: like all: but in parallelGravatar Enrico Tassi2016-06-17
* | Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Remove the syntax changes introduced by this branch.Gravatar Pierre-Marie Pédrot2016-06-15
| * | Allow `Pretyping.search_guard` to not check guardGravatar Arnaud Spiwack2016-06-15
* | | 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
|\ \ \ \ \
| | | | | * Admitted: fix #4818 return initial stmt and univsGravatar Matthieu Sozeau2016-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
* | | | | | STM: proof block detection for indentationGravatar Enrico Tassi2016-06-06
* | | | | | rebase on trunkGravatar Enrico Tassi2016-06-06
* | | | | | STM: fix error reporting of par:Gravatar Enrico Tassi2016-06-06
* | | | | | STM: proof block detection made optional + simple testGravatar Enrico Tassi2016-06-06
* | | | | | STM: proof block detection for par:Gravatar Enrico Tassi2016-06-06
* | | | | | STM: proof block detection for bullets and { block }Gravatar Enrico Tassi2016-06-06
* | | | | | STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
* | | | | | STM: carry AST and indentation of document commandsGravatar Enrico Tassi2016-06-06
* | | | | | STM: support for nested boxes of nodes to model error boundariesGravatar Enrico Tassi2016-06-06
* | | | | | STM: invalid states are first class citizensGravatar Enrico Tassi2016-06-06
| |/ / / / |/| | | |
* | | | | Move serialization functions out of StmGravatar Emilio Jesus Gallego Arias2016-06-02
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\ \ \ \ \ | | |_|_|/ | |/| | |
| | * | | STM delegation policy can be customizedGravatar Enrico Tassi2016-05-31
* | | | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| |/ / / |/| | |
| * | | STM: fix argument filtering for slavesGravatar Enrico Tassi2016-05-27
| * | | Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
* | | | typosGravatar Enrico Tassi2016-05-23
| | * | coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
| |/ / |/| |