X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionNaif.ml;h=987f4b6edbd8bc932207aeee2f493b2ea8135986;hb=77f5a051bb92b07456692fe70c2203d37a89a36d;hp=581c5918f4c78c301c1ba65009cc48aa2fc222da;hpb=eac698cf60e63383781fac2810981dface465216;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 581c5918f..987f4b6ed 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -54,7 +54,7 @@ let whd context =
        (match List.nth context (n-1) with
            Some (_, C.Decl _) -> if l = [] then t else C.Appl (t::l)
          | Some (_, C.Def bo) -> whdaux l (S.lift n bo)
-	 | None -> raise RelToHiddenHypothesis
+	  | None -> raise RelToHiddenHypothesis
        )
     | C.Var (uri,exp_named_subst) as t ->
        (match CicEnvironment.get_cooked_obj ~trust:false uri with