diff options
Diffstat (limited to 'tactics/abstract.mli')
| -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 9d4f3cfb27..0c74e898d2 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 |