aboutsummaryrefslogtreecommitdiff
path: root/library/lib.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-06-17 15:32:06 +0200
committerEmilio Jesus Gallego Arias2019-06-24 20:55:37 +0200
commitffaac25e993eaf103b5a66dd3b0bce7598ac8e15 (patch)
treea83b2c8e6848864d167d8992e5906308dcef40d9 /library/lib.ml
parent3f99dcacdf94e77395913973c8ae5cf5b9c65b35 (diff)
[proof] Move initial_euctx to proof_global
These are only needed when closing / admitting a proof.
Diffstat (limited to 'library/lib.ml')
0 files changed, 0 insertions, 0 deletions