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: make_still_working~6699
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eb41d84ee7ee6a53e35dd08e7fbf5d51f3972c4c;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/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 8ae5964c9..e1253f8e8 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/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