aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/obligations.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/obligations.mli')
-rw-r--r--toplevel/obligations.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index bc092a1ce..ddc99a96c 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -22,7 +22,7 @@ open Tacexpr
(** Forward declaration. *)
val declare_fix_ref : (definition_kind -> Id.t ->
- constr -> types -> Impargs.manual_implicits -> global_reference) ref
+ Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
val declare_definition_ref :
(Id.t -> definition_kind ->