aboutsummaryrefslogtreecommitdiff
path: root/tactics/abstract.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/abstract.mli')
-rw-r--r--tactics/abstract.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index c474a01d1c..e278729f89 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -26,5 +26,5 @@ val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit P
save path *)
val shrink_entry
: ('a, 'b) Context.Named.Declaration.pt list
- -> 'c Entries.definition_entry
- -> 'c Entries.definition_entry * Constr.t list
+ -> 'c Proof_global.proof_entry
+ -> 'c Proof_global.proof_entry * Constr.t list