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

7 files changed, 35 insertions, 32 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index a4a0cfa7ff..7c46619291 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -105,7 +105,7 @@ let lookup_tacs (hdc,c) (l,l',dn) =
 
 
 module Constr_map = Map.Make(struct 
-			       type t = constr_label
+			       type t = global_reference
 			       let compare = Pervasives.compare 
 			     end)
 
@@ -249,7 +249,7 @@ let make_resolve_hyp env sigma (hname,_,htyp) =
 
 (* REM : in most cases hintname = id *)
 let make_unfold (hintname, ref) =
-  (Pattern.label_of_ref ref,
+  (ref,
    { hname = hintname;
      pri = 4;
      pat = None;
@@ -305,7 +305,7 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
     }
   in
   let subst_hint (lab,data as hint) =
-    let lab' = subst_label subst lab in
+    let lab' = subst_global subst lab in
     let data' = match data.code with
       | Res_pf (c, clenv) ->
 	  let c' = subst_mps subst c in
@@ -511,13 +511,13 @@ let fmt_hint_list_for_head c =
       dbs 
   in
   if valid_dbs = [] then 
-    (str "No hint declared for :" ++ pr_ref_label c)
+    (str "No hint declared for :" ++ pr_global c)
   else 
     hov 0 
-      (str"For " ++ pr_ref_label c ++ str" -> " ++ fnl () ++
+      (str"For " ++ pr_global c ++ str" -> " ++ fnl () ++
 	 hov 0 (prlist fmt_hints_db valid_dbs))
 
-let fmt_hint_ref ref = fmt_hint_list_for_head (label_of_ref ref)
+let fmt_hint_ref ref = fmt_hint_list_for_head ref
 
 (* Print all hints associated to head id in any database *)
 let print_hint_ref ref =  ppnl(fmt_hint_ref ref)
@@ -562,7 +562,7 @@ let print_hint_db db =
   Hint_db.iter 
     (fun head hintlist ->
        msg (hov 0 
-	      (str "For " ++ pr_ref_label head ++ str " -> " ++
+	      (str "For " ++ pr_global head ++ str " -> " ++
 		 fmt_hint_list hintlist)))
     db
 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 68a8a3ba92..88be710c66 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -49,12 +49,12 @@ module Hint_db :
   sig
     type t
     val empty : t
-    val find : constr_label -> t -> search_entry
-    val map_all : constr_label -> t -> pri_auto_tactic list
-    val map_auto : constr_label * constr -> t -> pri_auto_tactic list
-    val add_one : constr_label * pri_auto_tactic -> t -> t
-    val add_list : (constr_label * pri_auto_tactic) list -> t -> t
-    val iter : (constr_label -> stored_data list -> unit) -> t -> unit
+    val find : global_reference -> t -> search_entry
+    val map_all : global_reference -> t -> pri_auto_tactic list
+    val map_auto : global_reference * constr -> t -> pri_auto_tactic list
+    val add_one : global_reference * pri_auto_tactic -> t -> t
+    val add_list : (global_reference * pri_auto_tactic) list -> t -> t
+    val iter : (global_reference -> stored_data list -> unit) -> t -> unit
   end
 
 type frozen_hint_db_table = Hint_db.t Stringmap.t
@@ -81,7 +81,7 @@ val searchtable : hint_db_table
    [ctyp] is the type of [hc]. *)
 
 val make_exact_entry :
-  identifier -> constr * constr -> constr_label * pri_auto_tactic
+  identifier -> constr * constr -> global_reference * pri_auto_tactic
 
 (* [make_apply_entry (eapply,verbose) name (c,cty)].
    [eapply] is true if this hint will be used only with EApply;
@@ -91,7 +91,7 @@ val make_exact_entry :
 
 val make_apply_entry :
   env -> evar_map -> bool * bool -> identifier -> constr * constr
-      -> constr_label * pri_auto_tactic
+      -> global_reference * pri_auto_tactic
 
 (* A constr which is Hint'ed will be:
    (1) used as an Exact, if it does not start with a product
@@ -102,7 +102,7 @@ val make_apply_entry :
 
 val make_resolves :
   env -> evar_map -> identifier -> bool * bool -> constr * constr -> 
-    (constr_label * pri_auto_tactic) list
+    (global_reference * pri_auto_tactic) list
 
 (* [make_resolve_hyp hname htyp].
    used to add an hypothesis to the local hint database;
@@ -111,13 +111,13 @@ val make_resolves :
 
 val make_resolve_hyp : 
   env -> evar_map -> named_declaration ->
-      (constr_label * pri_auto_tactic) list
+      (global_reference * pri_auto_tactic) list
 
 (* [make_extern name pri pattern tactic_expr] *)
 
 val make_extern :
   identifier -> int -> constr_pattern -> Tacexpr.glob_tactic_expr
-      -> constr_label * pri_auto_tactic
+      -> global_reference * pri_auto_tactic
 
 val set_extern_interp :
   (patvar_map -> Tacexpr.glob_tactic_expr -> tactic) -> unit
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 475a45e5d3..7d41ebf9df 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -11,6 +11,7 @@
 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
 
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 72c8f78cbd..cb042d4256 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;
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 00980d0fdc..8665cc7057 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -11,6 +11,7 @@
 (*i*)
 open Term
 open Pattern
+open Libnames
 (*i*)
 
 (* Named, bounded-depth, term-discrimination nets. *)
@@ -34,4 +35,4 @@ val freeze : ('na,'a) t -> ('na,'a) frozen_t
 val unfreeze : ('na,'a) frozen_t -> ('na,'a) t -> unit
 val empty : ('na,'a) t -> unit
 val to2lists : ('na,'a) t -> ('na * (constr_pattern * 'a)) list * 
-                             (constr_label option * 'a Btermdn.t) list
+                             (global_reference option * 'a Btermdn.t) list
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 9d9bcd2354..3ee0ee430d 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -21,7 +21,7 @@ open Nametab
    See the module dn.ml for further explanations.
    Eduardo (5/8/97) *)
 
-type 'a t = (constr_label,constr_pattern,'a) Dn.t
+type 'a t = (global_reference,constr_pattern,'a) Dn.t
 
 (*If we have: f a b c ..., decomp gives: (f,[a;b;c;...])*)
 
@@ -45,19 +45,18 @@ let constr_pat_discr t =
     None
   else
     match decomp_pat t with
-      | PRef (IndRef sp), args -> Some(IndNode sp,args)
-      | PRef (ConstructRef sp), args -> Some(CstrNode sp,args)
-      | PRef (VarRef id), args -> Some(VarNode id,args)
+      | PRef ((IndRef _) as ref), args
+      | PRef ((ConstructRef _ ) as ref), args
+      | PRef ((VarRef _) as ref), args -> Some(ref,args)
       | _ -> None
 
 let constr_val_discr t =
   let c, l = decomp t in
   match kind_of_term c with
     (* Const _,_) -> Some(TERM c,l) *)
-    | Ind ind_sp -> Some(IndNode ind_sp,l)
-    | Construct cstr_sp -> Some(CstrNode cstr_sp,l)
-    (* Ici, comment distinguer SectionVarNode de VarNode ?? *)
-    | Var id -> Some(VarNode id,l)
+    | Ind ind_sp -> Some(IndRef ind_sp,l)
+    | Construct cstr_sp -> Some(ConstructRef cstr_sp,l)
+    | Var id -> Some(VarRef id,l)
     | _ -> None
 
 (* Les deux fonctions suivantes ecrasaient les precedentes, 
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 6a6dfe3404..6e1bdd87ca 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -11,6 +11,7 @@
 (*i*)
 open Term
 open Pattern
+open Libnames
 (*i*)
   
 (* Discrimination nets of terms. *)
@@ -44,8 +45,8 @@ val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit
 (* These are for Nbtermdn *)
 
 val constr_pat_discr : 
-  constr_pattern -> (constr_label * constr_pattern list) option
+  constr_pattern -> (global_reference * constr_pattern list) option
 val constr_val_discr :
-  constr -> (constr_label * constr list) option
+  constr -> (global_reference * constr list) option
 
 (*i*)