aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.ml
Commit message (Expand)AuthorAge
* stm: feedback forwarding has to be atomicGravatar Enrico Tassi2016-09-13
* 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
* 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
* | | | 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/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
| * | STM delegation policy can be customizedGravatar Enrico Tassi2016-05-31
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
|/ /
| * coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
|/
* Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Gravatar Enrico Tassi2016-05-10
* STM: code cleanupGravatar Enrico Tassi2016-05-10
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\
| * Fix for #4603, part 3: definitions inside proofs not handled properly by coqc.Gravatar Maxime Dénès2016-05-04
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
| * Build stm debugging messages lazily so that they are not silentlyGravatar Hugo Herbelin2016-04-15
| * Quick fix for #4603 (part 2): Anomaly: Universe undefinedGravatar Maxime Dénès2016-04-12
* | Removing the dependency in VernacSolve in the STM.Gravatar Pierre-Marie Pédrot2016-03-19
* | Relying on Vernac classifier to flag tactics in the STM.Gravatar Pierre-Marie Pédrot2016-03-19
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-21
|\|
| * STM: Print/Extraction have to be skipped if -quickGravatar Enrico Tassi2016-02-19
| * STM: classify some variants of Instance as regular `Fork nodes.Gravatar Enrico Tassi2016-02-19
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \ \ | | |/ | |/|
| * | STM: always stock in vio files the first node (state) of a proofGravatar Enrico Tassi2016-02-10
| * | STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530Gravatar Enrico Tassi2016-02-10
| | * CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ |/|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-27 10:23:23 +0000