X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.ml;h=ac7441a4cdad4ee5f40fda81d3c0cf213cf7fb3e;hb=ed5c4e15429c37bef0f59dfd7160f6883586ed0f;hp=43e342e708f710ff27fcdb3f0aa41d00e6c4be5f;hpb=5da42f6120f3075c3da8ab3082ead39ea57955fa;p=helm.git

diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml
index 43e342e70..ac7441a4c 100644
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/components/cic_unification/coercGraph.ml
@@ -52,9 +52,9 @@ let saturate_coercion ul metasenv subst context =
     (fun arity (c,saturations) -> 
       let ty,_ =
        CicTypeChecker.type_of_aux' ~subst metasenv context c
-        CicUniv.empty_ugraph in
+        CicUniv.oblivion_ugraph in
       let _,metasenv,args,lastmeta =
-       TermUtil.saturate_term freshmeta metasenv context ty arity in
+       TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
       let irl =
        CicMkImplicit.identity_relocation_list_for_metavariable context
       in
@@ -158,7 +158,7 @@ let is_composite t =
       | Cic.Appl (he::_) -> CicUtil.uri_of_term he
       | _ -> CicUtil.uri_of_term t
     in
-    match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+    match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
     | Cic.Constant (_,_, _, _, attrs),_  ->
         List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
     | _ -> false
@@ -182,7 +182,7 @@ let coerced_arg l =
         | _ -> 0
       in
       let uri = CicUtil.uri_of_term c in
-      match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+      match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
       | Cic.Constant (_, _, ty, _, _) -> count_pi ty
       | _ -> assert false
     in