X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2FdoubleTypeInference.ml;h=214f656c38d5db4d27f889f9b6019b3b28d4eb12;hb=7dc9e84cd0e40d8ff6847aabe780a4196e30be36;hp=30a8f5c290fdaac79a3ecc28f10269f2d2db611f;hpb=db48e1ca9a2c0db7e8101367ec98e4ff2f1c069c;p=helm.git

diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml
index 30a8f5c29..214f656c3 100644
--- a/helm/software/components/cic_acic/doubleTypeInference.ml
+++ b/helm/software/components/cic_acic/doubleTypeInference.ml
@@ -319,6 +319,8 @@ let type_of_mutual_inductive_constr uri i j =
     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 ;;
 
+let pack_coercion = ref (fun _ _ _ -> assert false);;
+
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
  (* Coscoy's double type-inference algorithm             *)
@@ -330,6 +332,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
   let module R = CicReduction in
   let module S = CicSubstitution in
   let module U = UriManager in
+   let expectedty =
+    match expectedty with
+       None -> None
+     | Some t -> Some (!pack_coercion metasenv context t) in
    let synthesized =
     match t with
        C.Rel n ->
@@ -609,6 +615,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
            ty
    in
     let synthesized' = beta_reduce synthesized in
+    let synthesized' = !pack_coercion metasenv context synthesized' in
      let types,res =
       match expectedty with
          None ->