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/nbtermdn.ml | |
| parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) | |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'tactics/nbtermdn.ml')
| -rw-r--r-- | tactics/nbtermdn.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index bd4fb60e..0867d220 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nbtermdn.ml,v 1.7.16.1 2004/07/16 19:30:54 herbelin Exp $ *) +(* $Id: nbtermdn.ml 6427 2004-12-07 17:41:10Z sacerdot $ *) open Util open Names @@ -14,6 +14,7 @@ open Term open Libobject open Library open Pattern +open Libnames (* Named, bounded-depth, term-discrimination nets. Implementation: @@ -28,11 +29,11 @@ open Pattern type ('na,'a) t = { mutable table : ('na,constr_pattern * 'a) Gmap.t; - mutable patterns : (constr_label option,'a Btermdn.t) Gmap.t } + mutable patterns : (global_reference option,'a Btermdn.t) Gmap.t } type ('na,'a) frozen_t = ('na,constr_pattern * 'a) Gmap.t - * (constr_label option,'a Btermdn.t) Gmap.t + * (global_reference option,'a Btermdn.t) Gmap.t let create () = { table = Gmap.empty; |