X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fcompose.ml;h=317030404d12acd322676fd91e56cf05b3fe79c5;hb=42f2dc48b4fef5b404f406bf512d6a0cde35c067;hp=137e919b09fd98e6c5d6da3f5f155cd79b7850c6;hpb=c2a02fcbcaaef7358acebcb27014db4a601ad026;p=helm.git

diff --git a/components/tactics/compose.ml b/components/tactics/compose.ml
index 137e919b0..317030404 100644
--- 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 false
+            CicUniv.oblivion_ugraph saturations
         in
         assert (List.length menv1 = List.length menv);
         generate tl menv (t::acc)