From 6e17d968f26fe09938c3e825ee9e9a431e244350 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 4 Jun 2009 18:41:36 +0000 Subject: [PATCH] syntax error fixed :( --- helm/software/components/cic_acic/doubleTypeInference.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml index c60bf90f4..4ca88d4b9 100644 --- a/helm/software/components/cic_acic/doubleTypeInference.ml +++ b/helm/software/components/cic_acic/doubleTypeInference.ml @@ -378,7 +378,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = if does_not_occur 1 t_typ then (* since [Rel 1] does not occur in typ, substituting any term *) (* in place of [Rel 1] is equivalent to delifting once *) - CicSubstitution.subst (C.Implicit None) t_typ) + CicSubstitution.subst (C.Implicit None) t_typ else C.LetIn (n,s,ty,t_typ) | C.Appl (he::tl) when List.length tl > 0 -> -- 2.39.2