diff options
Diffstat (limited to 'tactics/nbtermdn.ml')
| -rw-r--r-- | tactics/nbtermdn.ml | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index 6459336b8..bafc85b12 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -104,19 +104,6 @@ let decomp = | Const _ -> Dn.Everything | _ -> Dn.Nothing -let constr_val_discr_st (idpred,cpred) t = - let c, l = decomp t in - match kind_of_term c with - | Const c -> if Cpred.mem c cpred then Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef c),l) - | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l) - | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l) - | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l) - | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c]) - | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l) - | Sort _ -> Dn.Label(Term_dn.SortLabel, []) - | Evar _ -> Dn.Everything - | _ -> Dn.Nothing - let lookup dn valu = let hkey = match (constr_val_discr valu) with |