Indentation + typo

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

6 files changed, 57 insertions, 58 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. *)
diff --git a/library/declare.ml b/library/declare.ml
index 343bc0c50..446e42d3c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -150,18 +150,18 @@ let open_constant i ((sp,kn),_) =
 let cache_constant ((sp,kn),(cdt,dhyps,imps,kind)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
-  if Idmap.mem id !vartab then
-    errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
-  if Nametab.exists_cci sp then
-    errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
-  let kn' = Global.add_constant dir id cdt in
-  assert (kn' = constant_of_kn kn);
-  Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
-  add_section_constant kn' (Global.lookup_constant kn').const_hyps;
-  Dischargedhypsmap.set_discharged_hyps sp dhyps;
-  with_implicits imps declare_constant_implicits kn';
-  Notation.declare_ref_arguments_scope (ConstRef kn');
-  csttab := Spmap.add sp kind !csttab
+    if Idmap.mem id !vartab then
+      errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+    if Nametab.exists_cci sp then
+      errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+    let kn' = Global.add_constant dir id cdt in
+      assert (kn' = constant_of_kn kn);
+      Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
+      add_section_constant kn' (Global.lookup_constant kn').const_hyps;
+      Dischargedhypsmap.set_discharged_hyps sp dhyps;
+      with_implicits imps declare_constant_implicits kn';
+      Notation.declare_ref_arguments_scope (ConstRef kn');
+      csttab := Spmap.add sp kind !csttab
 
 (*s Registration as global tables and rollback. *)
 
diff --git a/library/lib.ml b/library/lib.ml
index 0b383b34d..40590a220 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -186,9 +186,9 @@ let add_leaf id obj =
   if fst (current_prefix ()) = initial_path then 
     error ("No session module started (use -top dir)");
   let oname = make_oname id in
-  cache_object (oname,obj);
-  add_entry oname (Leaf obj);
-  oname
+    cache_object (oname,obj);
+    add_entry oname (Leaf obj);
+    oname
 
 let add_leaves id objs =
   let oname = make_oname id in
@@ -444,15 +444,15 @@ let open_section id =
   let dir = extend_dirpath olddir id in
   let prefix = dir, (mp, extend_dirpath oldsec id) in
   let name = make_path id, make_kn id (* this makes little sense however *) in
-  if Nametab.exists_section dir then
-    errorlabstrm "open_section" (pr_id id ++ str " already exists");
-  let sum = freeze_summaries() in
-  add_entry name (OpenedSection (prefix, sum));
-  (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
-  Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
-  path_prefix := prefix;
-  if !Options.xml_export then !xml_open_section id;
-  add_section ()
+    if Nametab.exists_section dir then
+      errorlabstrm "open_section" (pr_id id ++ str " already exists");
+    let sum = freeze_summaries() in
+      add_entry name (OpenedSection (prefix, sum));
+      (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
+      Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
+      path_prefix := prefix;
+      if !Options.xml_export then !xml_open_section id;
+      add_section ()
 
 
 (* Restore lib_stk and summaries as before the section opening, and
@@ -476,16 +476,16 @@ let close_section id =
       error "no opened section"
   in
   let (secdecls,_,before) = split_lib oname in
-  lib_stk := before;
-  let full_olddir = fst !path_prefix in
-  pop_path_prefix ();
-  add_entry (make_oname id) ClosedSection;
-  if !Options.xml_export then !xml_close_section id;
-  let newdecls = List.map discharge_item secdecls in
-  Summary.section_unfreeze_summaries fs;
-  List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls;
-  Cooking.clear_cooking_sharing ();
-  Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
+    lib_stk := before;
+    let full_olddir = fst !path_prefix in
+      pop_path_prefix ();
+      add_entry (make_oname id) ClosedSection;
+      if !Options.xml_export then !xml_close_section id;
+      let newdecls = List.map discharge_item secdecls in
+	Summary.section_unfreeze_summaries fs;
+	List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls;
+	Cooking.clear_cooking_sharing ();
+	Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
 
 (*****************)
 (* Backtracking. *)
diff --git a/library/libobject.ml b/library/libobject.ml
index b91cbe699..0a5379ee5 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -144,7 +144,7 @@ let apply_dyn_fun deflt f lobj =
 	  else
 	    anomaly
 	      ("Cannot find library functions for an object with tag "^tag) in 
-  	f dodecl
+	f dodecl
     with
 	Failure "local to_apply_dyn_fun" -> deflt;;
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 67b8e4398..cd6ce35cf 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1336,14 +1336,14 @@ End Fold_Right_Recursor.
       rewrite IHl; simpl; auto.
     Qed.
 
-    Lemma split_lenght_l : forall (l:list (A*B)),
+    Lemma split_length_l : forall (l:list (A*B)),
       length (fst (split l)) = length l. 
     Proof.
       induction l; simpl; auto.
       destruct a; destruct (split l); simpl; auto.
     Qed.
 
-    Lemma split_lenght_r : forall (l:list (A*B)),
+    Lemma split_length_r : forall (l:list (A*B)),
       length (snd (split l)) = length l. 
     Proof.
       induction l; simpl; auto.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 29f3b321f..09c63fc43 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -488,15 +488,14 @@ let vernac_end_section = Lib.close_section
 
 let vernac_end_segment id =
   check_no_pending_proofs ();
-  let o = 
-    try Lib.what_is_opened ()
-    with Not_found -> error "There is nothing to end." in
-  match o with
-    | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id
-    | _,Lib.OpenedModtype _ -> vernac_end_modtype id
-    | _,Lib.OpenedSection _ -> vernac_end_section id
-    | _ -> anomaly "No more opened things"
-      
+  let o = try Lib.what_is_opened () with 
+      Not_found -> error "There is nothing to end." in
+    match o with
+      | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id
+      | _,Lib.OpenedModtype _ -> vernac_end_modtype id
+      | _,Lib.OpenedSection _ -> vernac_end_section id
+      | _ -> anomaly "No more opened things"
+
 let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
   Library.require_library qidl import