From 22cb4d34d7f67eb98c737b076a4ecbbf800bdc55 Mon Sep 17 00:00:00 2001 From: sacerdot Date: Tue, 7 Dec 2004 17:41:10 +0000 Subject: 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 --- tactics/termdn.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'tactics/termdn.ml') 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, -- cgit v1.2.3