From a8e20a3995f4f90b742049dd682b25d831840d73 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 18 Feb 2006 18:20:02 +0000 Subject: [PATCH] Trivial bug fixed in the merging of polymorphic coercions. --- helm/software/components/library/cicCoercion.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml index 40def8238..7e36ac1aa 100644 --- a/helm/software/components/library/cicCoercion.ml +++ b/helm/software/components/library/cicCoercion.ml @@ -109,7 +109,7 @@ let generate_composite_closure rt c1 c2 univ = let rec aux = function | Cic.Lambda (_, Cic.Meta (i,_), t) when List.exists (fun (j,_,_) -> j = i) metasenv -> - CicSubstitution.subst (Cic.Rel ~-100) t + aux (CicSubstitution.subst (Cic.Rel ~-100) t) | Cic.Lambda (name, s, t) -> Cic.Lambda (name, s, aux t) | t -> t -- 2.39.2