From 4a0cd08598ce4b88b3c1d34b3beb3687eedb94f8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 12 Dec 2014 12:21:28 +0100
Subject: In discrimination nets, do not index lambdas if they're part of a
 beta redex.

---
 tactics/btermdn.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index ef813744e2..0eda410c1a 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
 
-- 
cgit v1.2.3