1. The last commit that fixed unification of compound coercions with

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 1caeb733db2a21253b996e91893f77df8a0d4878..620f66f1831a4ec598178645201dd7686c47c7d7 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -1115,9 +1115,25 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                            let newt, _, subst, metasenv, ugraph = 
                              avoid_double_coercion 
                               subst metasenv ugraph 
-                                (Cic.Appl[c;hete]) tgt_carr
-                           in
-                            newt, subst, metasenv, ugraph)
+                                (Cic.Appl[c;hete]) tgt_carr in
+                           try
+                            let newty,newhety,subst,metasenv,ugraph = 
+                              type_of_aux subst metasenv context newt ugraph in
+                            let subst,metasenv,ugraph1 = 
+                             fo_unif_subst subst context metasenv 
+                                newhety s ugraph
+                            in
+                             newt, subst, metasenv, ugraph
+                           with exn ->
+                            enrich localization_tbl hete
+                             ~f:(fun _ ->
+                               (lazy ("The term " ^
+                                 CicMetaSubst.ppterm_in_context subst hete
+                                  context ^ " has type " ^
+                                 CicMetaSubst.ppterm_in_context subst hety
+                                  context ^ " but is here used with type " ^
+                                 CicMetaSubst.ppterm_in_context subst s context
+                                  (* "\nReason: " ^ Lazy.force e*)))) exn)
                      | exn ->
                         enrich localization_tbl hete
                          ~f:(fun _ ->