diff options
| author | Pierre-Marie Pédrot | 2020-06-22 12:59:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-20 11:47:34 +0200 |
| commit | 4ebccb9d2722a7323cb7fce5c9e00bf2eea5b69f (patch) | |
| tree | ca132eb8ef2d3a30b8addb7633d3b263a1cdfb38 /tactics/btermdn.mli | |
| parent | b409b9837ce438042bb259d16a1b5156a2e0acb9 (diff) | |
Dnets now consider axioms as being opaque for pattern recognition.
Diffstat (limited to 'tactics/btermdn.mli')
| -rw-r--r-- | tactics/btermdn.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 2caa193202..ab201a1872 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -30,14 +30,14 @@ sig type pattern - val pattern : TransparentState.t option -> constr_pattern -> pattern + val pattern : Environ.env -> TransparentState.t option -> constr_pattern -> pattern val empty : t val add : t -> pattern -> Z.t -> t val rmv : t -> pattern -> Z.t -> t - val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list + val lookup : Environ.env -> Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list val app : (Z.t -> unit) -> t -> unit end |