X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcoercGraph.ml;h=f12ea14b108e447951fe3691556d9ed760b88c8d;hb=e68d06002f901a6252bc0b6ad6b655c9acb72b0f;hp=43e342e708f710ff27fcdb3f0aa41d00e6c4be5f;hpb=1d6910f6ee5dfd0e53fcec8c020311baba922a4c;p=helm.git diff --git a/components/cic_unification/coercGraph.ml b/components/cic_unification/coercGraph.ml index 43e342e70..f12ea14b1 100644 --- a/components/cic_unification/coercGraph.ml +++ b/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