From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 4 Jun 2009 18:41:36 +0000 (+0000)
Subject: syntax error fixed :(
X-Git-Tag: make_still_working~3919
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6e17d968f26fe09938c3e825ee9e9a431e244350;p=helm.git

syntax error fixed :(
---

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 ->