From 5af5db14a2bb7583ae1b8eaaf18ad26a06e3d892 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 Jun 2012 08:29:36 +0000 Subject: [PATCH] Reindented --- matita/components/ng_kernel/nCicTypeChecker.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) -- 2.39.2