diff options
-rw-r--r-- | tactics/btermdn.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index ef813744e..0eda410c1 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -74,7 +74,10 @@ let constr_val_discr_st (idpred,cpred) t = | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),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) + | Lambda (n, d, c) -> + if List.is_empty l then + Label(LambdaLabel, [d; c] @ l) + else Everything | Sort _ -> Label(SortLabel, []) | Evar _ -> Everything | _ -> Nothing @@ -90,7 +93,7 @@ let constr_pat_discr_st (idpred,cpred) t = | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) -> Some (GRLabel ref, args) | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c]) - | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l) + | PLambda (_, d, c), [] -> Some (LambdaLabel, [d ; c]) | PSort s, [] -> Some (SortLabel, []) | _ -> None |