aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Collapse)AuthorAge
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
| | | As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
| | | | We are left with the compatibility layer and a handful of primitives which require some thought to move.
* Fix -async-proofs-always-delegate (close 3740)Gravatar Enrico Tassi2014-10-15
|
* Stm: more precise representation of nested proofsGravatar Enrico Tassi2014-10-13
| | | | | | | | This fixes the bug reported by Hugo: 2) Goal True. 3-4) Definition a:=0. 5) Goal True True. (* jumped back to 3 (on master) instead of 4 (on the outermost proof) *)
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
|
* TQueue: new primitive to take a snapshot of the queueGravatar Enrico Tassi2014-10-13
|
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
| | | | | Now the seff contains it directly, no need to force the future or to hope that it is a Direct opaque proof.
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
| | | | | | | | | | | | | | Before this patch opaque tables were only growing, making them unusable in interactive mode (leak on Undo). With this patch the opaque tables are functional and part of the env. I.e. a constant_body can point to the proof term in 2 ways: 1) directly (before the constant is discharged) 2) indirectly, via an int, that is mapped by the opaque table to the proof term. This is now consistent in batch/interactive mode This is step 0 to make an interactive coqtop able to dump a .vo/.vi
* STM: report the (structured) goals as XMLGravatar Carst Tankink2014-10-01
| | | | | The leafs of the XML trees are still pretty-printed strings, but this could be refined later on.
* Add additional location information to AST XMLs.Gravatar Carst Tankink2014-10-01
|
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
| | | | | | | | will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise.
* XML pretty printing for AST (work by François Poulain, project DoCoq)Gravatar Enrico Tassi2014-09-29
| | | | It is not 100% complete, but the main part is there.
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
| | | | | | | | | | | so that one can retrieve them and pass them to third party tools (i.e. print the AST with the notations attached to the nodes concerned). Available syntax: - all in one: Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2"). - a posteriori: Format Notation "a /\ b" "latex" "#1 \wedge #2".
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
|
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
|
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
|
* Marshalling errors should be bold and red (should never happen actually)Gravatar Enrico Tassi2014-09-09
|
* A marshalling failure does not make a worker `OldGravatar Enrico Tassi2014-09-09
|
* Back: print subgoals as in 8.4 (Close: 3585)Gravatar Enrico Tassi2014-09-09
|
* BackTo not part of the doc when used by emacsGravatar Enrico Tassi2014-09-09
| | | | Used to work "by chance".
* Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Gravatar Enrico Tassi2014-09-09
|
* Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)Gravatar Enrico Tassi2014-09-09
|
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
| | | Dead code formerly used by the now defunct [autoinstances].
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
| | | | Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
* stm: use xlabel insted of label in dot (debug) outputGravatar Enrico Tassi2014-09-02
|
* coqworkmgrGravatar Enrico Tassi2014-09-02
|
* Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors inGravatar Matthieu Sozeau2014-08-26
| | | | stm test-suite files.
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
| | | | | par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
|
* STM: Classify Let as non asynchronous (Closes: #3486)Gravatar Enrico Tassi2014-08-05
|
* STM: when looking up in the cache catch Expired excGravatar Carst Tankink2014-08-04
|
* STM: generate Feedback message for parsing errorsGravatar Enrico Tassi2014-08-04
|
* STM: use a real priority queueGravatar Enrico Tassi2014-08-04
|
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
|
* STM: VtQuery holds the id of the state it refers toGravatar Carst Tankink2014-08-04
|
* STM: print goals with no duplicatesGravatar Enrico Tassi2014-07-29
|
* Fixing universe substitution in mutual fixpoints.Gravatar Pierre-Marie Pédrot2014-07-16
|
* STM: check-vi-task fixedGravatar Enrico Tassi2014-07-16
|
* STM: Goal printing got wrong in a merge, fixedGravatar Enrico Tassi2014-07-16
|
* STM: let toploop plugins specify the flags for STM workersGravatar Enrico Tassi2014-07-11
|
* STM: flag to turn off branch reopeningGravatar Enrico Tassi2014-07-11
| | | | This is useful if a UI does not support that
* STM: add optionally takes the id of the new tipGravatar Enrico Tassi2014-07-11
|
* STM: export the observe function (useful for pide)Gravatar Enrico Tassi2014-07-11
|
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
| | | | | LoadedFile is generated when a .vo is loaded Goals is generated when -feedback-goals
* Better handling of the universe context in case of Admitted proof obligations.Gravatar Matthieu Sozeau2014-07-10
|
* option to always delegate futures to workersGravatar Enrico Tassi2014-07-10
|
* more APIs in TQueue and CThreadGravatar Enrico Tassi2014-07-10
| | | | These are now sufficient to implement PIDE
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
|
* Patch from Enrico Tassi to get Drop compatible with stm.Gravatar Enrico Tassi2014-07-01
|
* Typo in stm error message.Gravatar Hugo Herbelin2014-06-28
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 18:45:01 +0000