From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 11 Jun 2012 08:29:36 +0000 (+0000)
Subject: Reindented
X-Git-Tag: make_still_working~1641
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5af5db14a2bb7583ae1b8eaaf18ad26a06e3d892;p=helm.git

Reindented
---

diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml
index 343be2607..e334861cb 100644
--- a/matita/components/ng_kernel/nCicTypeChecker.ml
+++ b/matita/components/ng_kernel/nCicTypeChecker.ml
@@ -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)