Skip to content

Commit 66e58e2

Browse files
committed
Fix ind_tables minimization
1 parent d3d4df8 commit 66e58e2

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

tactics/ind_tables.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -150,6 +150,7 @@ let define ?loc internal role id c poly uctx sch =
150150
let avoid = Id.Set.of_list @@ List.map (fun cst -> Constant.label cst) avoid in
151151
let id = compute_name internal id avoid in
152152
let uctx = UState.collapse_above_prop_sort_variables ~to_prop:true uctx in
153+
let uctx = UState.normalize_variables uctx in
153154
let uctx = UState.minimize uctx in
154155
let c = UState.nf_universes uctx c in
155156
let uctx = UState.restrict uctx (Vars.universes_of_constr c) in

0 commit comments

Comments
 (0)