diff options
| author | Emilio Jesus Gallego Arias | 2019-06-17 15:32:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:55:37 +0200 |
| commit | ffaac25e993eaf103b5a66dd3b0bce7598ac8e15 (patch) | |
| tree | a83b2c8e6848864d167d8992e5906308dcef40d9 /proofs/proof.mli | |
| parent | 3f99dcacdf94e77395913973c8ae5cf5b9c65b35 (diff) | |
[proof] Move initial_euctx to proof_global
These are only needed when closing / admitting a proof.
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index 6ef34eed80..7e535a258c 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -47,8 +47,6 @@ type data = (** A representation of the shelf *) ; given_up : Evar.t list (** A representation of the given up goals *) - ; initial_euctx : UState.t - (** The initial universe context (for the statement) *) ; name : Names.Id.t (** The name of the theorem whose proof is being constructed *) ; poly : bool; |