- let s' = CicReduction.normalize ~delta:false context s in
- res,(newmeta,context,s')::newmetasenv,newargument::arguments,lastmeta
- (** NORMALIZE RATIONALE
- * we normalize the target only NOW since we may be in this case:
- * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k
- * and we want a mesasenv with ?1:A1 and ?2:A2 and not
- * ?1, ?2, ?3 (that is the one we whould get if we start from the
- * beta-normalized A1 -> A2 -> A3 -> P **)
- | t -> (CicReduction.normalize ~delta:false context t),[],[],newmeta
+ if prod_no + 1 = goal_arity then
+ let head = CicReduction.normalize ~delta:false context ty in
+ head,[],[],lastmeta,goal_arity + 1
+ else
+ (** NORMALIZE RATIONALE
+ * we normalize the target only NOW since we may be in this case:
+ * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k
+ * and we want a mesasenv with ?1:A1 and ?2:A2 and not
+ * ?1, ?2, ?3 (that is the one we whould get if we start from the
+ * beta-normalized A1 -> A2 -> A3 -> P **)
+ let s' = CicReduction.normalize ~delta:false context s in
+ res,(newmeta,context,s')::newmetasenv,newargument::arguments,
+ lastmeta,prod_no + 1
+ | t ->
+ let head = CicReduction.normalize ~delta:false context t in
+ match CicReduction.whd context head with
+ C.Prod _ as head' -> aux newmeta head'
+ | _ -> head,[],[],newmeta,0