diff options
| author | Emilio Jesus Gallego Arias | 2019-02-24 01:57:59 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:13 +0200 |
| commit | a2ea73d84be2fe95eeda42f5f5ac458f0af9968f (patch) | |
| tree | 0b3c485f6e196bb74dca8c2eda6a6cf2448b2745 /vernac/comProgramFixpoint.ml | |
| parent | 5d18dfed8e68dd964bca5d64ca6bdd9f8ffbb1df (diff) | |
[proofs] Store hooks in the proof object.
As of now, hooks were stored in the terminators as closures, we place
them instead in the proof object and are thus passed back at proof
closing time.
This helps towards the reification and unification of terminators.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions