From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 4 Apr 2008 10:07:22 +0000 (+0000)
Subject: indentation fixed
X-Git-Tag: make_still_working~5457
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8cd2f04d5c46b4a1292fa840bc70e8f33676d1f7;p=helm.git

indentation fixed
---

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 _ ->