From 211bf1d85eeb8a0035d22dc29acad5411aed08cf Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 28 Oct 2006 17:12:31 +0000 Subject: [PATCH] GRAVE BUG IN COERCIONS FIXED: the insertion of a coercion used to introduce applications of applications (that are forbidden and not handled properly). --- components/cic_unification/cicRefine.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 8ae5964c9..e1253f8e8 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -325,7 +325,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let module S = CicSubstitution in let module U = UriManager in let try_coercion t subst metasenv context ugraph coercion_tgt c = - let coerced = C.Appl[c;t] in + let coerced = + match c with + C.Appl l2 -> C.Appl (l2@[t]) + | _ -> C.Appl [c;t] + in try let newt,_,subst,metasenv,ugraph = type_of_aux subst metasenv context coerced ugraph -- 2.39.2