Indentation + typo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9104 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 12 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 90317d531..264bd6215 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -134,21 +134,21 @@ let add_constant dir l decl senv =
   let kn = make_con senv.modinfo.modpath dir l in
   let cb = 
     match decl with 
-    | ConstantEntry ce -> translate_constant senv.env kn ce
-    | GlobalRecipe r ->
-	let cb = translate_recipe senv.env kn r in
-	if dir = empty_dirpath then hcons_constant_body cb else cb
+      | ConstantEntry ce -> translate_constant senv.env kn ce
+      | GlobalRecipe r ->
+	  let cb = translate_recipe senv.env kn r in
+	    if dir = empty_dirpath then hcons_constant_body cb else cb
   in
   let env' = Environ.add_constraints cb.const_constraints senv.env in
   let env'' = Environ.add_constant kn cb env' in
-  kn, { old = senv.old;
-	env = env'';
-	modinfo = senv.modinfo;
-	labset = Labset.add l senv.labset;
-	revsign = (l,SPBconst cb)::senv.revsign;
-	revstruct = (l,SEBconst cb)::senv.revstruct;
-	imports = senv.imports;
-	loads = senv.loads }
+    kn, { old = senv.old;
+	  env = env'';
+	  modinfo = senv.modinfo;
+	  labset = Labset.add l senv.labset;
+	  revsign = (l,SPBconst cb)::senv.revsign;
+	  revstruct = (l,SEBconst cb)::senv.revstruct;
+	  imports = senv.imports;
+	  loads = senv.loads }
     
 
 (* Insertion of inductive types. *)