From 85314379a501aa07fa6e7e2f0f66791deae27b40 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 12 Aug 2022 23:21:56 -0400 Subject: [PATCH] fix type of is_a --- src/base/Data_ty.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/base/Data_ty.ml b/src/base/Data_ty.ml index 6032707f..408e8dba 100644 --- a/src/base/Data_ty.ml +++ b/src/base/Data_ty.ml @@ -115,7 +115,6 @@ let cstor tst c : Term.t = List.map (fun s -> Lazy.force s.select_ty) (Lazy.force c.cstor_args) in let ty = Term.arrow_l tst ty_args ty_ret in - Log.debugf 50 (fun k -> k "cstor %a (ty %a)" Cstor.pp c Term.pp ty); Term.const tst @@ Const.make (Cstor c) ops ~ty let select tst s : Term.t = @@ -125,7 +124,9 @@ let select tst s : Term.t = Term.const tst @@ Const.make (Select s) ops ~ty let is_a tst c : Term.t = - Term.const tst @@ Const.make (Is_a c) ops ~ty:(Term.bool tst) + let ty_arg = Lazy.force c.cstor_ty in + let ty = Term.arrow tst ty_arg (Term.bool tst) in + Term.const tst @@ Const.make (Is_a c) ops ~ty let as_data t = match Term.view t with