From 28dc54e953e42f85e52a7f31c694b01907116841 Mon Sep 17 00:00:00 2001
From: Martin Clochard <martin.clochard@lri.fr>
Date: Tue, 12 Jan 2016 16:20:59 +0100
Subject: [PATCH] detect_polymorphism: must consider the return type of logic
symbols
---
src/transform/detect_polymorphism.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/transform/detect_polymorphism.ml b/src/transform/detect_polymorphism.ml
index f8c8d2ce93..9e6e11f3fd 100644
--- a/src/transform/detect_polymorphism.ml
+++ b/src/transform/detect_polymorphism.ml
@@ -50,7 +50,7 @@ let check_ls ign_ls ls =
List.fold_left
(fun acc ty -> acc || not (Ty.ty_closed ty))
false
- ls.Term.ls_args
+ (Opt.fold (fun acc x -> x :: acc) ls.Term.ls_args ls.Term.ls_value)
let detect_polymorphism_in_decl ign_ts ign_ls ign_pr d =
Debug.dprintf debug "[detect_polymorphism] |sts|=%d |sls|=%d |spr|=%d@."
--
GitLab