From a24bd8612b54327cb2a0d142fa899f4a81d27adb Mon Sep 17 00:00:00 2001 From: Soudant Date: Wed, 16 Apr 2025 09:47:11 +0200 Subject: [PATCH] Changed bound_names definition in rocq --- src/parametricity.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parametricity.ml b/src/parametricity.ml index d49b10b..cd3a724 100644 --- a/src/parametricity.ml +++ b/src/parametricity.ml @@ -1141,7 +1141,7 @@ let fix_template_params order evdr env temp b params = let cstrs = UVars.UContext.constraints uctx in let univs = Array.concat @@ Array.map_to_list map_univs univs in let cstrs = Univ.Constraints.fold fold_cstrs cstrs Univ.Constraints.empty in - let unames = Array.make (Array.length qvars) Anonymous, Array.make (Array.length univs) Anonymous in + let unames = { UVars.quals = Array.make (Array.length qvars) Anonymous; UVars.univs = Array.make (Array.length univs) Anonymous } in let uctx = UVars.UContext.make unames (UVars.Instance.of_array (qvars,univs), cstrs) in let default_univs = let qs, us = UVars.Instance.to_array temp.template_defaults in