diff options
Diffstat (limited to 'tactics/termdn.mli')
| -rw-r--r-- | tactics/termdn.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/termdn.mli b/tactics/termdn.mli index a9f11b3af..92a1b8c3e 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -14,7 +14,7 @@ open Pattern open Libnames open Names (*i*) - + (* Discrimination nets of terms. *) (* This module registers actions (typically tactics) mapped to patterns *) @@ -23,7 +23,7 @@ open Names 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 [transparent_state] +number of nodes of the patterns matching the term. The [transparent_state] indicates which constants and variables can be considered as rigid. These dnets are able to cope with existential variables as well, which match [Everything]. *) |