in
if prod_no + 1 = goal_arity then
let head = CicReduction.normalize ~delta:false context ty in
- head,[],[],newmeta,goal_arity + 1
+ head,[],[],lastmeta,goal_arity + 1
else
(** NORMALIZE RATIONALE
* we normalize the target only NOW since we may be in this case: