GRAVE BUG IN COERCIONS FIXED: the insertion of a coercion used to introduce

applications of applications (that are forbidden and not handled properly).

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 8ae5964c9cf209a8ba43ea65a1c9efcbd0329b40..e1253f8e8042cceec42add1498b88fe3986e0cef 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -325,7 +325,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
     let module S = CicSubstitution in
     let module U = UriManager in
     let try_coercion t subst metasenv context ugraph coercion_tgt c =
-      let coerced = C.Appl[c;t] in
+     let coerced =
+      match c with
+         C.Appl l2 -> C.Appl (l2@[t])
+       | _ -> C.Appl [c;t]
+     in
       try
         let newt,_,subst,metasenv,ugraph = 
           type_of_aux subst metasenv context coerced ugraph