diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/tactics/abstract.mli b/tactics/abstract.mli index 779e46cd49..c474a01d1c 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -20,3 +20,11 @@ val cache_term_by_tactic_then -> unit Proofview.tactic val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic + +(* Internal but used in a few places; should likely be made intro a + proper library function, or incorporated into the generic constant + save path *) +val shrink_entry + : ('a, 'b) Context.Named.Declaration.pt list + -> 'c Entries.definition_entry + -> 'c Entries.definition_entry * Constr.t list |