more transitivity on proofs

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 10563186461a2601c30d4799d7c6657db8231da0..1f92a5fa881b95396c1eaf06fd2a06fdcc0fc1fc 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1182,7 +1182,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                        (* we search a coercion from hety to s *)
                        let coer, tgt_carr = 
                          let carr t subst context = 
-                           CicMetaSubst.apply_subst subst t 
+                           CicReduction.whd ~delta:false 
+                             context (CicMetaSubst.apply_subst subst t )
                          in
                          let c_hety = carr hety subst context in
                          let c_s = carr s subst context in 
@@ -1489,32 +1490,29 @@ let pack_coercion metasenv ctx t =
    | C.LetIn (name,so,dest) -> 
        let ctx' = Some (name,(C.Def (so,None)))::ctx in
        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
-   | C.Appl l as t -> 
+   | C.Appl l -> 
+      let l = List.map (merge_coercions ctx) l in
+      let t = C.Appl l in
        let b,_,_,_ = is_a_double_coercion t in
        (* prerr_endline "CANDIDATO!!!!"; *)
-       let newt = 
-         if b then
-           let ugraph = CicUniv.empty_ugraph in
-           let old_insert_coercions = !insert_coercions in
-           insert_coercions := false;
-           let newt, _, menv, _ = 
-             try 
-               type_of_aux' metasenv ctx t ugraph 
-             with RefineFailure _ | Uncertain _ -> 
-               prerr_endline (CicPp.ppterm t);
-               t, t, [], ugraph 
-           in
-           insert_coercions := old_insert_coercions;
-           if metasenv <> [] || menv = [] then 
-             newt 
-           else 
-             (prerr_endline "PUO' SUCCEDERE!!!!!";t)
-         else
-           t
-       in
-       (match newt with
-       | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l)
-       | _ -> assert false)
+       if b then
+         let ugraph = CicUniv.empty_ugraph in
+         let old_insert_coercions = !insert_coercions in
+         insert_coercions := false;
+         let newt, _, menv, _ = 
+           try 
+             type_of_aux' metasenv ctx t ugraph 
+           with RefineFailure _ | Uncertain _ -> 
+             prerr_endline (CicPp.ppterm t);
+             t, t, [], ugraph 
+         in
+         insert_coercions := old_insert_coercions;
+         if metasenv <> [] || menv = [] then 
+           newt 
+         else 
+           (prerr_endline "PUO' SUCCEDERE!!!!!";t)
+       else
+         t
    | C.Var (uri,exp_named_subst) -> 
        let exp_named_subst = List.map aux exp_named_subst in
        C.Var (uri, exp_named_subst)
@@ -1648,3 +1646,5 @@ let type_of_aux' ?localization_tbl metasenv context term ugraph =
 
 let typecheck ~localization_tbl metasenv uri obj =
  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
+
+let _ = DoubleTypeInference.pack_coercion := pack_coercion;;