added oblivion_universe and used it in paxck_coercions

[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 95651c49fe96ff9ebddec5eed4a8463422b5d67e..9cb0a04a43b8c5c55c34a224248e078f73f8f9ce 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1763,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)
@@ -1773,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, _ =