diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 03:21:18 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:17:16 -0400 |
| commit | 49b559ccb6d17b5356bc0e43c81a8363ec0b4768 (patch) | |
| tree | acd69f445ed5e60fe21002fa29bd2a65bbd7b02f | |
| parent | dc5f5f911177bc3bee518f1557b7665bc0e06d5a (diff) | |
[proof] Fixme on unused return type.
| -rw-r--r-- | tactics/proof_global.ml | 3 | ||||
| -rw-r--r-- | tactics/proof_global.mli | 5 |
2 files changed, 3 insertions, 5 deletions
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index bbf1d0d019..fe2f828fb4 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -118,8 +118,7 @@ let set_used_variables ps l = Environ.fold_named_context aux env ~init:(ctx,ctx_set) in if not (Option.is_empty ps.section_vars) then CErrors.user_err Pp.(str "Used section variables can be declared only once"); - (* EJGA: This is always empty thus we should modify the type *) - (ctx, []), { ps with section_vars = Some (Context.Named.to_vars ctx) } + ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) } let get_open_goals ps = let Proof.{ goals; stack; shelf } = Proof.data ps.proof in diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index 339a7f1898..59881dffa1 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -94,7 +94,6 @@ val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) val set_endline_tactic : Genarg.glob_generic_argument -> t -> t (** Sets the section variables assumed by the proof, returns its closure - * (w.r.t. type dependencies and let-ins covered by it) + a list of - * ids to be cleared *) + * (w.r.t. type dependencies and let-ins covered by it) *) val set_used_variables : t -> - Names.Id.t list -> (Constr.named_context * Names.lident list) * t + Names.Id.t list -> Constr.named_context * t |