diff options
| author | Carst Tankink | 2014-09-30 11:03:12 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-01 18:08:51 +0200 |
| commit | 9a3abe5b18a84733c0c01c2647108196798a761c (patch) | |
| tree | fb14d51392aa666e31ba40a0db396f7dcfd6192c /lib/cArray.ml | |
| parent | c73a59d9a6f124d5668054a16057d0955ca43cbd (diff) | |
Factored out IDE goal structure.
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.
Diffstat (limited to 'lib/cArray.ml')
0 files changed, 0 insertions, 0 deletions