]> matita.cs.unibo.it Git - helm.git/commitdiff
Reindentation.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 27 Jun 2003 15:37:53 +0000 (15:37 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 27 Jun 2003 15:37:53 +0000 (15:37 +0000)
helm/ocaml/cic_proof_checking/cicReductionNaif.ml

index 581c5918f4c78c301c1ba65009cc48aa2fc222da..987f4b6edbd8bc932207aeee2f493b2ea8135986 100644 (file)
@@ -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