| CicUnification.Uncertain _ -> false, menv2, m
in
(* check which "positions" in the input arrow unifies with saturated_ty2 *)
- let rec positions menv cur arity = function
+ let rec positions menv cur saturations = function
| Cic.Prod (n,s,t) ->
let b, newmenv, sb = unif menv s in
if b then
- (arity - cur - 1) ::
- (positions newmenv (cur + 1) arity (CicSubstitution.subst sb t))
+ (saturations - cur - 1) ::
+ (positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t))
else
- positions newmenv (cur + 1) arity (CicSubstitution.subst sb t)
+ positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t)
| _ -> []
in
- (* position is a list of arities, that is if t1 : a -> b -> c and arity is
+ (* position is a list of arities, that is if t1 : a -> b -> c and saturations is
* 0 then the computed term will be (t1 ? t2) of type a -> c
- * if arity is 1 then (t1 t2 ?) of type b -> c *)
+ * if saturations is 1 then (t1 t2 ?) of type b -> c *)
let rec generate positions menv acc =
match positions with
| [] -> acc, menv
- | arity::tl ->
+ | saturations::tl ->
try
let t, menv1, _ =
CloseCoercionGraph.generate_composite t2 t1 context menv
- CicUniv.oblivion_ugraph arity
+ CicUniv.oblivion_ugraph saturations
in
assert (List.length menv1 = List.length menv);
generate tl menv (t::acc)