diff options
Diffstat (limited to 'tactics/btermdn.ml')
| -rw-r--r-- | tactics/btermdn.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index c5cdd540..f0b23b8d 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -6,11 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: btermdn.ml,v 1.5.16.1 2004/07/16 19:30:52 herbelin Exp $ *) +(* $Id: btermdn.ml 6427 2004-12-07 17:41:10Z sacerdot $ *) open Term open Termdn open Pattern +open Libnames (* Discrimination nets with bounded depth. See the module dn.ml for further explanations. @@ -34,7 +35,7 @@ let bounded_constr_val_discr (t,depth) = | None -> None | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) -type 'a t = (constr_label,constr_pattern * int,'a) Dn.t +type 'a t = (global_reference,constr_pattern * int,'a) Dn.t let create = Dn.create |