diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
| commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
| tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /tactics/btermdn.ml | |
| parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) | |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
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 |