Removing Termdn, and putting the relevant code in Btermdn. The current Termdn

file was useless and duplicated code from Btermdn itself.

1 files changed, 12 insertions, 0 deletions

diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index fedc68047..575502026 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -11,6 +11,18 @@ open Pattern
 open Names
 
 (** Discrimination nets with bounded depth. *)
+
+(** This module registers actions (typically tactics) mapped to patterns *)
+
+(** Patterns are stocked linearly as the list of its node in prefix
+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]
+indicates which constants and variables can be considered as rigid.
+These dnets are able to cope with existential variables as well, which match
+[Everything]. *)
+
 module Make :
   functor (Z : Map.OrderedType) ->
 sig