X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=9cb0a04a43b8c5c55c34a224248e078f73f8f9ce;hb=77d56df4d446307199a9d4e03478260c6c63baf8;hp=4fc9f4cccdc80e943ee6bc5367e8e24f7f37dbf6;hpb=5d010a40c726d9a7eceeb35e70e41a158eb63c70;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 4fc9f4ccc..9cb0a04a4 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1332,7 +1332,12 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
             he
         in
         let x,xty,subst,metasenv,ugraph =
-            type_of_aux subst metasenv context x ugraph
+         (*CSC: here unsharing is necessary to avoid an unwanted
+           relocalization. However, this also shows a great source of
+           inefficiency: "x" is refined twice (once now and once in the
+           subsequent eat_prods_and_args). Morevoer, how is divergence avoided?
+         *)
+         type_of_aux subst metasenv context (Unshare.unshare x) ugraph
         in
         let carr_src = 
           CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty) 
@@ -1758,7 +1763,7 @@ let pack_coercion metasenv ctx t =
    | C.LetIn (name,so,dest) -> 
        let _,ty,metasenv,ugraph =
         pack_coercions := false;
-        type_of_aux' metasenv ctx so CicUniv.empty_ugraph in
+        type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
         pack_coercions := true;
        let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
@@ -1768,7 +1773,7 @@ let pack_coercion metasenv ctx t =
        let b,_,_,_,_ = is_a_double_coercion t in
        (* prerr_endline "CANDIDATO!!!!"; *)
        if b then
-         let ugraph = CicUniv.empty_ugraph in
+         let ugraph = CicUniv.oblivion_ugraph in
          let old_insert_coercions = !insert_coercions in
          insert_coercions := false;
          let newt, _, menv, _ =