diff options
Diffstat (limited to 'proofs/goal.mli')
| -rw-r--r-- | proofs/goal.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index 6b587959a..4cd3e4746 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -111,7 +111,7 @@ val clear_body : Names.Id.t list -> subgoals sensitive (* Changes an hypothesis of the goal with a convertible type and body. Checks convertibility if the boolean argument is true. *) -val convert_hyp : bool -> Term.named_declaration -> subgoals sensitive +val convert_hyp : bool -> Context.named_declaration -> subgoals sensitive (* Changes the conclusion of the goal with a convertible type and body. Checks convertibility if the boolean argument is true. *) |