diff options
| author | Pierre-Marie Pédrot | 2020-09-18 10:11:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-18 11:43:45 +0200 |
| commit | f50bbdc50b21083f65f0e415e7f2edff6f11e45f (patch) | |
| tree | d146dadf7fbe1ceb2f7ae7d031d0f0b0a85bc0a0 /tactics/btermdn.mli | |
| parent | 41b407395ba6f2ce2db5dd9365c9cbcb04a4e7c0 (diff) | |
Remove unused API from Dn.
Diffstat (limited to 'tactics/btermdn.mli')
| -rw-r--r-- | tactics/btermdn.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index ab201a1872..01d68a8045 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -38,7 +38,6 @@ sig val rmv : t -> pattern -> Z.t -> t val lookup : Environ.env -> Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list - val app : (Z.t -> unit) -> t -> unit end val dnet_depth : int ref |