From 8696083d0d696402d4cd06ac010f5a5eac0689f4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 27 Jun 2024 14:58:14 +0200 Subject: [PATCH] Adapt to coq/coq#19233 (template_universes don't duplicate level data) --- src/parametricity.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/parametricity.ml b/src/parametricity.ml index 08c3494..49d14a1 100644 --- a/src/parametricity.ml +++ b/src/parametricity.ml @@ -1064,17 +1064,17 @@ let get_arity t = (* Workaround to ensure that template universe levels are linear *) let fix_template_params order evdr env temp b params = - let templ = List.rev temp.template_param_levels in + let templ = List.rev temp.template_param_arguments in (* For all template levels generate fresh levels for all translated parameters *) let rec freshen umap templ params = match templ with | [] -> let () = assert (List.is_empty params) in umap, [] - | None :: templ -> + | false :: templ -> let decls, params = List.chop (order + 1) params in let umap, params = freshen umap templ params in umap, decls @ params - | Some _ :: templ -> + | true :: templ -> let decls, params = List.chop (order + 1) params in let umap, params = freshen umap templ params in let rel, pdecls = match decls with