From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 tactics/termdn.mli | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

(limited to 'tactics/termdn.mli')

diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index b65c0eeb..79efd8eb 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -6,12 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: termdn.mli 6427 2004-12-07 17:41:10Z sacerdot $ i*)
+(*i $Id: termdn.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Term
 open Pattern
 open Libnames
+open Names
 (*i*)
   
 (* Discrimination nets of terms. *)
@@ -22,7 +23,10 @@ open Libnames
 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 *)
+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]. *)
 
 type 'a t
 
@@ -30,13 +34,13 @@ val create : unit -> 'a t
 
 (* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *)
 
-val add : 'a t -> (constr_pattern * 'a) -> 'a t
+val add : 'a t -> transparent_state -> (constr_pattern * 'a) -> 'a t
 
-val rmv : 'a t -> (constr_pattern * 'a) -> 'a t
+val rmv : 'a t -> transparent_state -> (constr_pattern * 'a) -> 'a t
 
 (* [lookup t c] looks for patterns (with their action) matching term [c] *)
 
-val lookup : 'a t -> constr -> (constr_pattern * 'a) list
+val lookup : 'a t -> transparent_state -> constr -> (constr_pattern * 'a) list
 
 val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit
 
@@ -44,9 +48,12 @@ val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit
 (*i*)
 (* These are for Nbtermdn *)
 
-val constr_pat_discr : 
+val constr_pat_discr_st : transparent_state ->
   constr_pattern -> (global_reference * constr_pattern list) option
-val constr_val_discr :
-  constr -> (global_reference * constr list) option
+val constr_val_discr_st : transparent_state ->
+  constr -> (global_reference * constr list) Dn.lookup_res
+
+val constr_pat_discr : constr_pattern -> (global_reference * constr_pattern list) option
+val constr_val_discr : constr -> (global_reference * constr list) Dn.lookup_res
 
 (*i*)
-- 
cgit v1.2.3