From 8cd2f04d5c46b4a1292fa840bc70e8f33676d1f7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Apr 2008 10:07:22 +0000 Subject: [PATCH] indentation fixed --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 5e4000740..e6a5cbbc2 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -887,10 +887,10 @@ let rec typeof ~subst ~metasenv context term = let type_t = typeof_aux context t in if not (R.are_convertible ~subst ~metasenv context type_t ct) then raise (TypeCheckerFailure - (lazy (Printf.sprintf - ("Not well typed metavariable local context: "^^ - "expected a term of type %s, found %s of type %s") - (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t)))) + (lazy (Printf.sprintf + ("Not well typed metavariable local context: "^^ + "expected a term of type %s, found %s of type %s") + (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t)))) ) l lifted_canonical_context with Invalid_argument _ -> -- 2.39.2