From ead129a76cb3ceb656b60556bf10f38c667ce45a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 2 Mar 2020 16:29:51 +0100
Subject: Generalize the Ltac2 value criterion to pure let-bindings.

---
 user-contrib/Ltac2/tac2intern.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index ecea0a9903..797f72702d 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -396,11 +396,13 @@ let is_pure_constructor kn =
 
 let rec is_value = function
 | GTacAtm (AtmInt _) | GTacVar _ | GTacRef _ | GTacFun _ -> true
-| GTacAtm (AtmStr _) | GTacApp _ | GTacLet _ -> false
+| GTacAtm (AtmStr _) | GTacApp _ | GTacLet (true, _, _) -> false
 | GTacCst (Tuple _, _, el) -> List.for_all is_value el
 | GTacCst (_, _, []) -> true
 | GTacOpn (_, el) -> List.for_all is_value el
 | GTacCst (Other kn, _, el) -> is_pure_constructor kn && List.for_all is_value el
+| GTacLet (false, bnd, e) ->
+  is_value e && List.for_all (fun (_, e) -> is_value e) bnd
 | GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _
 | GTacWth _ -> false
 
-- 
cgit v1.2.3