Ugly solution to the "we proved T that is equivalent to T" problem:

[helm.git] / helm / software / components / cic_acic / doubleTypeInference.ml

diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml
index 30a8f5c290fdaac79a3ecc28f10269f2d2db611f..214f656c38d5db4d27f889f9b6019b3b28d4eb12 100644 (file)
--- 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 ->