Skip to content

Commit 937537d

Browse files
authored
Merge pull request #137 from LeoAlexElouan/clarify-bound-names
adapt to rocq-prover/rocq#20496 (changed bound_names)
2 parents 3301779 + a24bd86 commit 937537d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/parametricity.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1141,7 +1141,7 @@ let fix_template_params order evdr env temp b params =
11411141
let cstrs = UVars.UContext.constraints uctx in
11421142
let univs = Array.concat @@ Array.map_to_list map_univs univs in
11431143
let cstrs = Univ.Constraints.fold fold_cstrs cstrs Univ.Constraints.empty in
1144-
let unames = Array.make (Array.length qvars) Anonymous, Array.make (Array.length univs) Anonymous in
1144+
let unames = { UVars.quals = Array.make (Array.length qvars) Anonymous; UVars.univs = Array.make (Array.length univs) Anonymous } in
11451145
let uctx = UVars.UContext.make unames (UVars.Instance.of_array (qvars,univs), cstrs) in
11461146
let default_univs =
11471147
let qs, us = UVars.Instance.to_array temp.template_defaults in

0 commit comments

Comments
 (0)