From 9a1fa3669e18e6316df66c76a7316aa6a1826157 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Dec 2008 10:02:11 +0000 Subject: [PATCH] identity coercions are not really inserted, just used as hints for unification --- .../components/cic_unification/cicRefine.ml | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 245c88e00..a2c770749 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1444,11 +1444,19 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci let newt,newhety,subst,metasenv,ugraph = type_of_aux subst metasenv context c ugraph in let newt, newty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv ugraph newt expty + avoid_double_coercion context subst metasenv ugraph newt + expty in let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv newhety expty ugraph in - Some ((newt,newty), subst, metasenv, ugraph) + fo_unif_subst subst context metasenv newhety expty ugraph + in + let b, ugraph = + CicReduction.are_convertible ~subst context infty expty ugraph + in + if b then + Some ((t,infty), subst, metasenv, ugraph) + else + Some ((newt,newty), subst, metasenv, ugraph) with | Uncertain _ -> uncertain := true; None | RefineFailure _ -> None) -- 2.39.2