diff options
| author | Emilio Jesus Gallego Arias | 2019-02-24 02:24:47 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:13 +0200 |
| commit | a296e879112f2e88b2fdfbf2fe90f1807f90b890 (patch) | |
| tree | 8a0bd991117086222175377bb01ee2a70b904258 /vernac/vernacentries.mli | |
| parent | a2ea73d84be2fe95eeda42f5f5ac458f0af9968f (diff) | |
[proof] Unify obligation proof save path: Part I, declareObl
We move obligation declaration-specific functions to their own
file. This way, `Lemmas` can access them, and in the next part we can
factorize common parts in the save proof.
Diffstat (limited to 'vernac/vernacentries.mli')
0 files changed, 0 insertions, 0 deletions