| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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/ | |||
| 2014-06-25 | cut toploop(s) out of coqtop: now they are loaded dynamically | Enrico Tassi | |
| User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/ and pass -toploop footop to customize the coq main loop. A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to functions respectively initializing the toploop (and parsing toploop specific arguments) and running the main loop itself. For backward compatibility -ideslave and -async-proofs worker do set the toploop to coqidetop and stmworkertop respectively. | |||
| 2014-06-23 | Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344) | Enrico Tassi | |
| Every time you use abstract a kitten dies, please stop. | |||
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | |
| and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup. | |||
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot | |
| 2014-06-08 | Moving hook code from Future to Lemmas. This seemed to disrupt compilation of | Pierre-Marie Pédrot | |
| the checker, and it was not used before that anyway. | |||
| 2014-06-08 | Enforce a correct exception handling in declaration_hooks | Enrico Tassi | |
| This should finally get rid of the following class of bugs: Qed fails, STM undoes to the beginning of the proof because the exception is not annotated with the correct state, PG gets out of sync because errors always refer to the last command in PGIP. | |||
| 2014-06-08 | STM: handle "Time Abort" correctly (Closes: 3332) | Enrico Tassi | |
| 2014-06-06 | Remove the syntax [Vernac1. Vernac2. … Vernacn. ]. | Arnaud Spiwack | |
| It grouped a list of vernac commands as a single one. It was undocumented and unused (and apparently unusable, because the intermediate '.' seem to be parsed as end of phrases by the interfaces). The main application could be to group the commands for Time. There is room for such an application in the syntax, but I unplugged the syntax for the time being. The syntax would conflict with the use of a standalone dispatching tactical [ t1 | t2 | … | tn ]. I took the opportunity to separate the code dedicated to lists of commands in a separate type from vernac_expr. | |||
