aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-02-24 02:24:47 +0100
committerEmilio Jesus Gallego Arias2019-06-17 12:30:13 +0200
commita296e879112f2e88b2fdfbf2fe90f1807f90b890 (patch)
tree8a0bd991117086222175377bb01ee2a70b904258 /proofs
parenta2ea73d84be2fe95eeda42f5f5ac458f0af9968f (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 'proofs')
0 files changed, 0 insertions, 0 deletions