From 22a5700f44c6156571e0aa9c67a04995a7c68f99 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 3 May 2024 09:59:20 +0200 Subject: [PATCH] Adapt w.r.t. coq/coq#18996. --- src/debug.ml | 7 +------ src/parametricity.ml | 8 +------- 2 files changed, 2 insertions(+), 13 deletions(-) diff --git a/src/debug.ml b/src/debug.ml index 2f90c3f..67ac2ce 100644 --- a/src/debug.ml +++ b/src/debug.ml @@ -106,15 +106,10 @@ let debug_case_info flags ci = let ndecls = String.concat ";" (List.map string_of_int (Array.to_list ci.ci_cstr_ndecls)) in let nargs = String.concat ";" (List.map string_of_int (Array.to_list ci.ci_cstr_nargs)) in let pp_info x = - let ind_tags = String.concat ";" (List.map string_of_bool x.ind_tags) in - let cstr_tags = - String.concat "," (List.map (fun tags -> String.concat ";" (List.map string_of_bool tags)) - (Array.to_list x.cstr_tags)) - in let string_of_style = match x.style with LetStyle -> "LetStyle" | IfStyle -> "IfStyle" | LetPatternStyle -> "LetPatternStyle" | MatchStyle -> "MatchStyle" | RegularStyle -> "RegularStyle" in - Printf.sprintf "ind_tags = %s, cstr_tags = %s, style = %s" ind_tags cstr_tags string_of_style + Printf.sprintf "style = %s" string_of_style in debug_string flags (Printf.sprintf "CASEINFO:inductive = %s.\nparam = %d.\nndecls = %s.\nnargs = %s.\npp_info = %s\n.EOFCASEINFO" diff --git a/src/parametricity.ml b/src/parametricity.ml index 2fb2ccb..bdc217d 100644 --- a/src/parametricity.ml +++ b/src/parametricity.ml @@ -553,13 +553,7 @@ and translate_case_info order env ci = } and translate_case_printing order env cp = - let translate_bool_list l = - List.flatten (List.map (fun x -> range (fun _ -> x) (order + 1)) l) - in - { - ind_tags = (range (fun _ -> false) order) @ translate_bool_list cp.ind_tags; - cstr_tags = Array.map translate_bool_list cp.cstr_tags; - style = translate_style cp.style } + { style = translate_style cp.style } and translate_style x = x