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

11 files changed, 43 insertions, 81 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 757b61aa1..dcaac5697 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -142,11 +142,6 @@ let pr_rawterm t =
   else Ppconstrnew.pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)
 
 open Pattern
-let pr_ref_label = function (* On triche sur le contexte *)
-  | ConstNode sp -> pr_constant (Global.env()) sp
-  | IndNode sp -> pr_inductive (Global.env()) sp
-  | CstrNode sp -> pr_constructor (Global.env()) sp
-  | VarNode id -> pr_id id
 
 let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t
 
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 04c61ed05..22b5daa17 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -45,7 +45,6 @@ val pr_existential  : env -> existential -> std_ppcmds
 val pr_constructor  : env -> constructor -> std_ppcmds
 val pr_inductive    : env -> inductive -> std_ppcmds
 val pr_global       : global_reference -> std_ppcmds
-val pr_ref_label    : constr_label -> std_ppcmds
 val pr_pattern      : constr_pattern -> std_ppcmds
 val pr_pattern_env  : env -> names_context -> constr_pattern -> std_ppcmds
 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index cea07c6b6..b091d797a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -114,41 +114,16 @@ let rec subst_pattern subst pat = match pat with
 	if cofixpoint' == cofixpoint then pat else
 	  PCoFix cofixpoint'
 
-type constr_label =
-  | ConstNode of constant
-  | IndNode of inductive
-  | CstrNode of constructor
-  | VarNode of identifier
-
 exception BoundPattern;;
 
-let label_of_ref = function
-  | ConstRef sp     -> ConstNode sp
-  | IndRef sp       -> IndNode sp
-  | ConstructRef sp -> CstrNode sp
-  | VarRef id       -> VarNode id
-
-let ref_of_label = function
-  | ConstNode sp     -> ConstRef sp
-  | IndNode sp       -> IndRef sp
-  | CstrNode sp      -> ConstructRef sp
-  | VarNode id       -> VarRef id
-
-let subst_label subst cstl = 
-  let ref = ref_of_label cstl in
-  let ref' = subst_global subst ref in
-    if ref' == ref then cstl else
-      label_of_ref ref'
-      
-  
 let rec head_pattern_bound t =
   match t with
     | PProd (_,_,b)  -> head_pattern_bound b 
     | PLetIn (_,_,b) -> head_pattern_bound b 
     | PApp (c,args)  -> head_pattern_bound c
     | PCase (_,p,c,br) -> head_pattern_bound c
-    | PRef r         -> label_of_ref r
-    | PVar id        -> VarNode id
+    | PRef r         -> r
+    | PVar id        -> VarRef id
     | PEvar _ | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _
 	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
@@ -156,10 +131,10 @@ let rec head_pattern_bound t =
     | PCoFix _ -> anomaly "head_pattern_bound: not a type"
 
 let head_of_constr_reference c = match kind_of_term c with
-  | Const sp -> ConstNode sp
-  | Construct sp -> CstrNode sp
-  | Ind sp -> IndNode sp
-  | Var id -> VarNode id
+  | Const sp -> ConstRef sp
+  | Construct sp -> ConstructRef sp
+  | Ind sp -> IndRef sp
+  | Var id -> VarRef id
   | _ -> anomaly "Not a rigid reference"
 
 let rec pattern_of_constr t =
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 398117303..7ce0c4124 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -52,28 +52,18 @@ val occur_meta_pattern : constr_pattern -> bool
 
 val subst_pattern : substitution -> constr_pattern -> constr_pattern
 
-type constr_label =
-  | ConstNode of constant
-  | IndNode of inductive
-  | CstrNode of constructor
-  | VarNode of identifier
-
-val label_of_ref : global_reference -> constr_label
-
-val subst_label : substitution -> constr_label -> constr_label
-
 exception BoundPattern
 
 (* [head_pattern_bound t] extracts the head variable/constant of the
    type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly
    if [t] is an abstraction *)
 
-val head_pattern_bound : constr_pattern -> constr_label
+val head_pattern_bound : constr_pattern -> global_reference
 
 (* [head_of_constr_reference c] assumes [r] denotes a reference and
    returns its label; raises an anomaly otherwise *)
 
-val head_of_constr_reference : Term.constr -> constr_label
+val head_of_constr_reference : Term.constr -> global_reference
 
 (* [pattern_of_constr c] translates a term [c] with metavariables into
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
diff --git a/tactics/auto.ml b/tactics/auto.ml
index a4a0cfa7f..7c4661929 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 68a8a3ba9..88be710c6 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 475a45e5d..7d41ebf9d 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 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;
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 00980d0fd..8665cc705 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 9d9bcd235..3ee0ee430 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 6a6dfe340..6e1bdd87c 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*)