diff options
| author | Pierre-Marie Pédrot | 2018-11-19 08:12:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:29:55 +0100 |
| commit | 733cb74a2038ff92156b7209713fc2ea741ccca6 (patch) | |
| tree | ee664936850ce6160d9e3fc3219b9dba7b7ea096 /tactics/btermdn.mli | |
| parent | ad5aea737ecc639c31dda84322b3550a4d380b47 (diff) | |
Rename TranspState into TransparentState.
Diffstat (limited to 'tactics/btermdn.mli')
| -rw-r--r-- | tactics/btermdn.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 6af5012def..cc31fb0599 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -18,7 +18,7 @@ open Pattern order in such a way patterns having the same prefix have this common prefix shared and the seek for the action associated to the patterns that a term matches are found in time proportional to the maximal -number of nodes of the patterns matching the term. The [TranspState.t] +number of nodes of the patterns matching the term. The [TransparentState.t] indicates which constants and variables can be considered as rigid. These dnets are able to cope with existential variables as well, which match [Everything]. *) @@ -30,10 +30,10 @@ sig val empty : t - val add : TranspState.t option -> t -> (constr_pattern * Z.t) -> t - val rmv : TranspState.t option -> t -> (constr_pattern * Z.t) -> t + val add : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t + val rmv : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t - val lookup : Evd.evar_map -> TranspState.t option -> t -> EConstr.constr -> Z.t list + val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list val app : (Z.t -> unit) -> t -> unit end |