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, 7 insertions, 8 deletions

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,