X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.ml;h=f12ea14b108e447951fe3691556d9ed760b88c8d;hb=08e9d02504942642a917c0d3e4b4795e65172d89;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..f12ea14b1 100644
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/components/cic_unification/coercGraph.ml
@@ -54,7 +54,7 @@ let saturate_coercion ul metasenv subst context =
        CicTypeChecker.type_of_aux' ~subst metasenv context c
         CicUniv.empty_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