diff options
author | 2012-12-14 15:56:25 +0000 | |
---|---|---|
committer | 2012-12-14 15:56:25 +0000 | |
commit | 67f5c70a480c95cfb819fc68439781b5e5e95794 (patch) | |
tree | 67b88843ba54b4aefc7f604e18e3a71ec7202fd3 /tactics/termdn.ml | |
parent | cc03a5f82efa451b6827af9a9b42cee356ed4f8a (diff) |
Modulification of identifier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/termdn.ml')
-rw-r--r-- | tactics/termdn.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 268c6a2e8..becd19a66 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -85,9 +85,9 @@ let constr_pat_discr_st (idpred,cpred) t = match decomp_pat t with | PRef ((IndRef _) as ref), args | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) - | PRef ((VarRef v) as ref), args when not (Idpred.mem v idpred) -> + | PRef ((VarRef v) as ref), args when not (Id.Pred.mem v idpred) -> Some(GRLabel ref,args) - | PVar v, args when not (Idpred.mem v idpred) -> + | PVar v, args when not (Id.Pred.mem v idpred) -> Some(GRLabel (VarRef v),args) | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) -> Some (GRLabel ref, args) @@ -113,7 +113,7 @@ let constr_val_discr_st (idpred,cpred) t = | Const c -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l) | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l) | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l) - | Var id when not (Idpred.mem id idpred) -> Label(GRLabel (VarRef id),l) + | Var id when not (Id.Pred.mem id idpred) -> Label(GRLabel (VarRef id),l) | Prod (n, d, c) -> Label(ProdLabel, [d; c]) | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l) | Sort _ -> Label (SortLabel, []) |