diff options
Diffstat (limited to 'plugins/subtac/subtac_obligations.mli')
| -rw-r--r-- | plugins/subtac/subtac_obligations.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli index bc5fc3e1..5f6d1a2e 100644 --- a/plugins/subtac/subtac_obligations.mli +++ b/plugins/subtac/subtac_obligations.mli @@ -6,9 +6,9 @@ open Proof_type open Vernacexpr type obligation_info = - (identifier * Term.types * loc * + (identifier * Term.types * hole_kind located * obligation_definition_status * Intset.t * tactic option) array - (* ident, type, location, (opaque or transparent, expand or define), + (* ident, type, source, (opaque or transparent, expand or define), dependencies, tactic to solve it *) type progress = (* Resolution status of a program *) |