]> matita.cs.unibo.it Git - helm.git/commitdiff
Reindented
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 11 Jun 2012 08:29:36 +0000 (08:29 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 11 Jun 2012 08:29:36 +0000 (08:29 +0000)
matita/components/ng_kernel/nCicTypeChecker.ml

index 343be2607277b7bbab8e4bd0523fc35d9d7d0069..e334861cbf9c0482f02e8e7401f6fb24e8b7f4c6 100644 (file)
@@ -1131,7 +1131,7 @@ and get_relevance status ~metasenv ~subst context t args =
               | C.Sort C.Prop ->
                   false::(aux context new_ty tl)
               | C.Sort _
-                   | C.Meta _ -> true::(aux context new_ty tl)
+              | C.Meta _ -> true::(aux context new_ty tl)
               | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
                      "Prod: the type %s of the source of %s is not a sort" 
                       (status#ppterm ~subst ~metasenv ~context sort)