From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 28 Oct 2006 17:12:31 +0000 (+0000)
Subject: GRAVE BUG IN COERCIONS FIXED: the insertion of a coercion used to introduce
X-Git-Tag: 0.4.95@7852~840
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=211bf1d85eeb8a0035d22dc29acad5411aed08cf;p=helm.git

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 8ae5964c9..e1253f8e8 100644
--- 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