From 583b5c104e1f1c44e8d7b6a840f97134987d7898 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Tue, 7 Jun 2011 18:12:06 +0200 Subject: [PATCH] fix an insufficient check in Discriminate.Lsmap.add --- src/transform/discriminate.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/transform/discriminate.ml b/src/transform/discriminate.ml index 5c93d5bf1..dc2ba1da0 100644 --- a/src/transform/discriminate.ml +++ b/src/transform/discriminate.ml @@ -57,7 +57,7 @@ module Lsmap = struct let add ls tyl tyv lsmap = if ls_equal ls ps_equ then lsmap else - if not (List.for_all Ty.ty_closed tyl) then lsmap else + if not (List.for_all Ty.ty_closed (oty_cons tyl tyv)) then lsmap else let newls = function | None -> Some (create_lsymbol (id_clone ls.ls_name) tyl tyv) | nls -> nls -- GitLab