]> matita.cs.unibo.it Git - helm.git/commitdiff
syntax error fixed :(
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 4 Jun 2009 18:41:36 +0000 (18:41 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 4 Jun 2009 18:41:36 +0000 (18:41 +0000)
helm/software/components/cic_acic/doubleTypeInference.ml

index c60bf90f46b738ff13e996d503ea3ac689a68148..4ca88d4b96a411318a6be88d2c6c1ef4d9e6302c 100644 (file)
@@ -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 ->