The type Pattern.constr_label was isomorphic to Libnames.global_reference.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6427 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 2 deletions

diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 72c8f78cb..cb042d425 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -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;