diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-12 12:21:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-12 12:21:28 +0100 |
| commit | 4a0cd08598ce4b88b3c1d34b3beb3687eedb94f8 (patch) | |
| tree | 77fbd2cd1f394d1424f753c340e6c6d67fa21d21 /tactics/btermdn.ml | |
| parent | dbe6df0d591bc6ac843360a3998f947d56298d4f (diff) | |
In discrimination nets, do not index lambdas if they're part of a beta
redex.
Diffstat (limited to 'tactics/btermdn.ml')
| -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 |