diff options
| author | Maxime Dénès | 2020-06-11 18:51:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-08-26 16:38:34 +0200 |
| commit | 46c0b7ab3653a6f1ef4b40466c2dd130d09136cb (patch) | |
| tree | b6937b47990e5f76b3f9a5b0fc8999754334ce26 /proofs/proof.mli | |
| parent | 4e59a68fd6f2cd3cdf936c10cdbfeb46fc22ca95 (diff) | |
Move given_up goals to evar_map
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 2d4966676e..a0d4759bfc 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -45,8 +45,6 @@ type data = (** A representation of the focus stack *) ; shelf : Evar.t list (** A representation of the shelf *) - ; given_up : Evar.t list - (** A representation of the given up goals *) ; name : Names.Id.t (** The name of the theorem whose proof is being constructed *) ; poly : bool; |