diff options
| author | Emilio Jesus Gallego Arias | 2019-06-11 02:16:51 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:14 +0200 |
| commit | 75e7c5b596d2a3e9b54e84788a15299568792584 (patch) | |
| tree | 6b326ec3279535bcad3f5bcbe0080679b2621dfb /tactics | |
| parent | 0ad30b6fce3eb757d06808e160a4c92e45686072 (diff) | |
[equations] [proof] Remove duplicate shrink function.
Equation's terminator had exactly duplicated the shrink function used
in `Abstract`, we remove this duplicity.
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 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 |