From 05616ce0c63bc4d766d5958d71f95ee49658c446 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 20 Jan 2025 14:54:54 +0100
Subject: [PATCH] [Eva] Add support for assigns \empty without \from
---
src/plugins/eva/engine/transfer_specification.ml | 13 ++++++++++++-
1 file changed, 12 insertions(+), 1 deletion(-)
diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml
index 1539cc63406..4697b7f2671 100644
--- a/src/plugins/eva/engine/transfer_specification.ml
+++ b/src/plugins/eva/engine/transfer_specification.ml
@@ -46,7 +46,18 @@ let warn_empty_assigns () =
(* Warn for assigns clauses without \from. *)
let warn_empty_from list =
- let no_from = List.filter (fun (_, from) -> from = FromAny) list in
+ let is_empty_set it =
+ match it with
+ | { it_content = { term_node = Tempty_set }} -> true
+ | _ -> false
+ in
+ let no_from =
+ List.filter
+ (fun (it, from) ->
+ (* Ignore assigns \empty with no \from. *)
+ not (is_empty_set it) && from = FromAny)
+ list
+ in
match no_from with
| [] -> ()
| (out, _) :: _ ->
--
GitLab