pack_coercion used to avoid packing n-ary coercions where n > 2.

Fixed.

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 10563186461a2601c30d4799d7c6657db8231da0..6065d24bd41a705fba4f977ea28dd18b919c9300 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1489,32 +1489,29 @@ let pack_coercion metasenv ctx t =
    | C.LetIn (name,so,dest) -> 
        let ctx' = Some (name,(C.Def (so,None)))::ctx in
        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
-   | C.Appl l as t -> 
+   | C.Appl l -> 
+      let l = List.map (merge_coercions ctx) l in
+      let t = C.Appl l in
        let b,_,_,_ = is_a_double_coercion t in
        (* prerr_endline "CANDIDATO!!!!"; *)
-       let newt = 
-         if b then
-           let ugraph = CicUniv.empty_ugraph in
-           let old_insert_coercions = !insert_coercions in
-           insert_coercions := false;
-           let newt, _, menv, _ = 
-             try 
-               type_of_aux' metasenv ctx t ugraph 
-             with RefineFailure _ | Uncertain _ -> 
-               prerr_endline (CicPp.ppterm t);
-               t, t, [], ugraph 
-           in
-           insert_coercions := old_insert_coercions;
-           if metasenv <> [] || menv = [] then 
-             newt 
-           else 
-             (prerr_endline "PUO' SUCCEDERE!!!!!";t)
-         else
-           t
-       in
-       (match newt with
-       | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l)
-       | _ -> assert false)
+       if b then
+         let ugraph = CicUniv.empty_ugraph in
+         let old_insert_coercions = !insert_coercions in
+         insert_coercions := false;
+         let newt, _, menv, _ = 
+           try 
+             type_of_aux' metasenv ctx t ugraph 
+           with RefineFailure _ | Uncertain _ -> 
+             prerr_endline (CicPp.ppterm t);
+             t, t, [], ugraph 
+         in
+         insert_coercions := old_insert_coercions;
+         if metasenv <> [] || menv = [] then 
+           newt 
+         else 
+           (prerr_endline "PUO' SUCCEDERE!!!!!";t)
+       else
+         t
    | C.Var (uri,exp_named_subst) -> 
        let exp_named_subst = List.map aux exp_named_subst in
        C.Var (uri, exp_named_subst)