diff options
| author | Pierre-Marie Pédrot | 2021-01-20 20:05:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-20 22:22:28 +0100 |
| commit | c9e1d6971fc9652ef1114dc4c2a3efa207ac8fbd (patch) | |
| tree | f65e369ef7397e11af5ac5562fb59e11a6006425 /lib | |
| parent | ae46681fcd8c07d4feca66c0940c83446791d8b0 (diff) | |
Slightly less stupid algorithm for simpl fixpoint expansion.
Instead of storing the bare fixpoint and its unfolded body in the term,
incurring a cost for their lifts under contexts, we simply store them
in the side map used to track the relation between a fresh problem evar
and its minimal arity. We also replace the hacky evarmap used to track
instantiation with a mere set.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions