X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=5aa96944d4e50295cac8094e69210f75e5cff99b;hb=ebb2f4bda5f7c5c7fc26d3aa1e17312f8900da4a;hp=065dbc33d9cd8a3e2d6a6a175962809e63a9997e;hpb=97b18234921aec71a8b89ec2c1b058e12e5e043c;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 065dbc33d..5aa96944d 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -649,7 +649,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                (let candidate,ugraph5,metasenv,subst = 
                  let exp_name_subst, metasenv = 
                     let o,_ = 
-                      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri 
+                      CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri 
                     in
                     let uris = CicUtil.params_of_obj o in
                     List.fold_right (
@@ -1847,7 +1847,7 @@ let are_all_occurrences_positive metasenv ugraph uri tys leftno =
   metasenv,ugraph,substituted_tys
     
 let typecheck metasenv uri obj ~localization_tbl =
- let ugraph = CicUniv.empty_ugraph in
+ let ugraph = CicUniv.oblivion_ugraph in
  match obj with
     Cic.Constant (name,Some bo,ty,args,attrs) ->
      (* CSC: ugly code. Here I need to retrieve in advance the loc of bo