aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Expand)AuthorAge
* 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
|\ \ \ \
| | * | | 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
| |/ / |/| |
* | | Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | 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
* | | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\ \ \
* \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\ \ \ \ | | |/ / | |/| |
| * | | Univs: fix get_current_context (bug #4603, part I)Gravatar Matthieu Sozeau2016-03-25
* | | | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
* | | | 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-03-18
|\| | |
| * | | Tentative fix for bug #4614: "Fully check the document" is uninterruptable.Gravatar Pierre-Marie Pédrot2016-03-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 21:03:27 +0000