diff options
| author | Pierre-Marie Pédrot | 2015-02-21 17:53:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-21 18:48:15 +0100 |
| commit | eeb2164e9a7d705e9cc82009d5c0f6a3528726b2 (patch) | |
| tree | 76a8cc64b00bc3d161a6badf21e1f4ac6051ee1e /dev/base_include | |
| parent | dd888dffd48fbf74a83b9f3c07bbdeb63dc020a2 (diff) | |
More resilient implementation of Print Assumptions.
Instead of registering all the transitive dependencies of a term in one go,
we rather recursively build the graph of direct dependencies of this term.
This is finer-grained and offers a better API.
The traversal now uses the standard term fold operation, and also registers
inductives and constructors encountered in the traversal.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions