Composition of coercions with arity > 0 is now implemented correctly.

[helm.git] / components / tactics / compose.ml

diff --git a/components/tactics/compose.ml b/components/tactics/compose.ml
index cd355dc2785049d44dd78630401ea1884a052087..317030404d12acd322676fd91e56cf05b3fe79c5 100644 (file)
--- a/components/tactics/compose.ml
+++ b/components/tactics/compose.ml
@@ -59,27 +59,27 @@ let compose_core t2 t1 (proof, goal) =
     | 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)