| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Factored out IDE goal structure. |  Carst Tankink | 2014-10-01 |
| | | | | | | | | | | | | | The more structured goal record type of CoqIDE is also useful for other interfaces (in particular, for PIDE). To support this, the datatype was factored out to the Proof module. In addition, the record gains a type parameter, to allow interfaces to adapt the output to their needs. To accommodate this type, the Proof module also gains the map_structured_proof that takes a Proof.proof and a function on the individual goals (in the context of an evar map) and produces a structured goal based on the goal transformer. | ||
| * | CoqIDE: new message to print AST |  Enrico Tassi | 2014-09-29 |
| | | |||
| * | STM: code restructured to reuse task queue for tactics | Enrico Tassi | 2014-08-05 |
| | | |||
| * | all coqide specific files moved into ide/ | Enrico Tassi | 2014-06-25 |
| 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 Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |