| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-10-16 | Goal: remove most of the API (make [Goal.goal] concrete). | Arnaud Spiwack | |
| We are left with the compatibility layer and a handful of primitives which require some thought to move. | |||
| 2014-10-15 | Fix -async-proofs-always-delegate (close 3740) | Enrico Tassi | |
| 2014-10-13 | Stm: more precise representation of nested proofs | Enrico Tassi | |
| 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) *) | |||
| 2014-10-13 | STM: primitives to snapshot a .vi while in interactive mode | Enrico Tassi | |
| 2014-10-13 | TQueue: new primitive to take a snapshot of the queue | Enrico Tassi | |
| 2014-10-13 | STM: simplify how the term part of a side effect is retrieved | Enrico Tassi | |
| Now the seff contains it directly, no need to force the future or to hope that it is a Direct opaque proof. | |||
| 2014-10-13 | library/opaqueTables: enable their use in interactive mode | Enrico Tassi | |
| 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 | |||
| 2014-10-01 | STM: report the (structured) goals as XML | Carst Tankink | |
| The leafs of the XML trees are still pretty-printed strings, but this could be refined later on. | |||
| 2014-10-01 | Add additional location information to AST XMLs. | Carst Tankink | |
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin | |
| 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. | |||
| 2014-09-29 | XML pretty printing for AST (work by François Poulain, project DoCoq) | Enrico Tassi | |
| It is not 100% complete, but the main part is there. | |||
| 2014-09-29 | Notation: option to attach extra pretty printing rules to notations | Enrico Tassi | |
| 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". | |||
| 2014-09-16 | Undo prints only if coqtop || emacs | Enrico Tassi | |
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin | |
| 2014-09-10 | VernacExtend does not dispatch on type anymore. | Pierre-Marie Pédrot | |
| 2014-09-09 | Marshalling errors should be bold and red (should never happen actually) | Enrico Tassi | |
| 2014-09-09 | A marshalling failure does not make a worker `Old | Enrico Tassi | |
| 2014-09-09 | Back: print subgoals as in 8.4 (Close: 3585) | Enrico Tassi | |
| 2014-09-09 | BackTo not part of the doc when used by emacs | Enrico Tassi | |
| Used to work "by chance". | |||
| 2014-09-09 | Undo: if the ui is coqtop (command line) then Undo is not part of the doc. | Enrico Tassi | |
| 2014-09-09 | Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407) | Enrico Tassi | |
| 2014-09-04 | Remove [Infer] option of records. | Arnaud Spiwack | |
| Dead code formerly used by the now defunct [autoinstances]. | |||
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack | |
| 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. | |||
| 2014-09-02 | stm: use xlabel insted of label in dot (debug) output | Enrico Tassi | |
| 2014-09-02 | coqworkmgr | Enrico Tassi | |
| 2014-08-26 | Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors in | Matthieu Sozeau | |
| stm test-suite files. | |||
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi | |
| par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2). | |||
| 2014-08-05 | STM: code restructured to reuse task queue for tactics | Enrico Tassi | |
| 2014-08-05 | STM: Classify Let as non asynchronous (Closes: #3486) | Enrico Tassi | |
| 2014-08-04 | STM: when looking up in the cache catch Expired exc | Carst Tankink | |
| 2014-08-04 | STM: generate Feedback message for parsing errors | Enrico Tassi | |
| 2014-08-04 | STM: use a real priority queue | Enrico Tassi | |
| 2014-08-04 | STM: encapsulate Pp.message in Feedback.feedback | Carst Tankink | |
| 2014-08-04 | STM: VtQuery holds the id of the state it refers to | Carst Tankink | |
| 2014-07-29 | STM: print goals with no duplicates | Enrico Tassi | |
| 2014-07-16 | Fixing universe substitution in mutual fixpoints. | Pierre-Marie Pédrot | |
| 2014-07-16 | STM: check-vi-task fixed | Enrico Tassi | |
| 2014-07-16 | STM: Goal printing got wrong in a merge, fixed | Enrico Tassi | |
| 2014-07-11 | STM: let toploop plugins specify the flags for STM workers | Enrico Tassi | |
| 2014-07-11 | STM: flag to turn off branch reopening | Enrico Tassi | |
| This is useful if a UI does not support that | |||
| 2014-07-11 | STM: add optionally takes the id of the new tip | Enrico Tassi | |
| 2014-07-11 | STM: export the observe function (useful for pide) | Enrico Tassi | |
| 2014-07-11 | Feedback: LoadedFile + Goals | Enrico Tassi | |
| LoadedFile is generated when a .vo is loaded Goals is generated when -feedback-goals | |||
| 2014-07-10 | Better handling of the universe context in case of Admitted proof obligations. | Matthieu Sozeau | |
| 2014-07-10 | option to always delegate futures to workers | Enrico Tassi | |
| 2014-07-10 | more APIs in TQueue and CThread | Enrico Tassi | |
| These are now sufficient to implement PIDE | |||
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | |
| 2014-07-01 | Patch from Enrico Tassi to get Drop compatible with stm. | Enrico Tassi | |
| 2014-06-28 | Typo in stm error message. | Hugo Herbelin | |
| 2014-06-25 | all coqide specific files moved into ide/ | Enrico Tassi | |
| lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/ | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |