diff options
| author | Emilio Jesus Gallego Arias | 2020-06-23 21:48:23 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:12 +0200 |
| commit | bf31fad28992a67b66d859655f030e619b69705e (patch) | |
| tree | 878e41ee13f2891edf19ed6ad25b29ed11f03264 /vernac/comProgramFixpoint.ml | |
| parent | ea8b9e060dfba9cc8706677e29c26dabaaa87551 (diff) | |
[declare] Improve logical code order
Now that the interface has mostly stabilized, we move code around to
respect internal dependency order.
This will allow us to start sharing more code in the 4 principal
cases, and also paves the way for the full merging of obligations and
the removal of the Proof_ending type in favor of stronger type
abstraction.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions