diff options
| author | Pierre-Marie Pédrot | 2020-03-02 16:29:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-11 13:24:50 +0200 |
| commit | ead129a76cb3ceb656b60556bf10f38c667ce45a (patch) | |
| tree | a16633b2a9bb11c0b35a5fc07b4ae288deece873 | |
| parent | 457cee4345ab4ad6b6624a6886841fd0b0739b2a (diff) | |
Generalize the Ltac2 value criterion to pure let-bindings.
| -rw-r--r-- | user-contrib/Ltac2/tac2intern.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |