aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Collapse)Author
2014-10-01Add additional location information to AST XMLs.Carst Tankink
2014-09-30Add 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-29XML 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-29Notation: option to attach extra pretty printing rules to notationsEnrico 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-16Undo prints only if coqtop || emacsEnrico Tassi
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-10VernacExtend does not dispatch on type anymore.Pierre-Marie Pédrot
2014-09-09Marshalling errors should be bold and red (should never happen actually)Enrico Tassi
2014-09-09A marshalling failure does not make a worker `OldEnrico Tassi
2014-09-09Back: print subgoals as in 8.4 (Close: 3585)Enrico Tassi
2014-09-09BackTo not part of the doc when used by emacsEnrico Tassi
Used to work "by chance".
2014-09-09Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Enrico Tassi
2014-09-09Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)Enrico Tassi
2014-09-04Remove [Infer] option of records.Arnaud Spiwack
Dead code formerly used by the now defunct [autoinstances].
2014-09-04Print [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-02stm: use xlabel insted of label in dot (debug) outputEnrico Tassi
2014-09-02coqworkmgrEnrico Tassi
2014-08-26Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors inMatthieu Sozeau
stm test-suite files.
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
2014-08-05STM: code restructured to reuse task queue for tacticsEnrico Tassi
2014-08-05STM: Classify Let as non asynchronous (Closes: #3486)Enrico Tassi
2014-08-04STM: when looking up in the cache catch Expired excCarst Tankink
2014-08-04STM: generate Feedback message for parsing errorsEnrico Tassi
2014-08-04STM: use a real priority queueEnrico Tassi
2014-08-04STM: encapsulate Pp.message in Feedback.feedbackCarst Tankink
2014-08-04STM: VtQuery holds the id of the state it refers toCarst Tankink
2014-07-29STM: print goals with no duplicatesEnrico Tassi
2014-07-16Fixing universe substitution in mutual fixpoints.Pierre-Marie Pédrot
2014-07-16STM: check-vi-task fixedEnrico Tassi
2014-07-16STM: Goal printing got wrong in a merge, fixedEnrico Tassi
2014-07-11STM: let toploop plugins specify the flags for STM workersEnrico Tassi
2014-07-11STM: flag to turn off branch reopeningEnrico Tassi
This is useful if a UI does not support that
2014-07-11STM: add optionally takes the id of the new tipEnrico Tassi
2014-07-11STM: export the observe function (useful for pide)Enrico Tassi
2014-07-11Feedback: LoadedFile + GoalsEnrico Tassi
LoadedFile is generated when a .vo is loaded Goals is generated when -feedback-goals
2014-07-10Better handling of the universe context in case of Admitted proof obligations.Matthieu Sozeau
2014-07-10option to always delegate futures to workersEnrico Tassi
2014-07-10more APIs in TQueue and CThreadEnrico Tassi
These are now sufficient to implement PIDE
2014-07-01Add toplevel commands to declare global universes and constraints.Matthieu Sozeau
2014-07-01Patch from Enrico Tassi to get Drop compatible with stm.Enrico Tassi
2014-06-28Typo in stm error message.Hugo Herbelin
2014-06-25all 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-25cut toploop(s) out of coqtop: now they are loaded dynamicallyEnrico 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-23Fix 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-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu 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-17Removing dead code.Pierre-Marie Pédrot
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
the checker, and it was not used before that anyway.
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico 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-08STM: handle "Time Abort" correctly (Closes: 3332)Enrico Tassi
2014-06-06Remove 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.