diff options
| author | Hugo Herbelin | 2020-09-19 18:02:42 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-19 18:02:42 +0200 |
| commit | fff4fe1120c81ab7b543cfb8d175cc4458e3c12e (patch) | |
| tree | f6600997d01306f371526b905e5dfaf26c0f4afd /tactics/btermdn.mli | |
| parent | 9809e48867867b26844656a1368dcb88a83c36ed (diff) | |
| parent | f50bbdc50b21083f65f0e415e7f2edff6f11e45f (diff) | |
Merge PR #13052: Clean up Dnet implementation
Reviewed-by: herbelin
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 |