Indentation + typo

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

3 files changed, 35 insertions, 35 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 343bc0c508..446e42d3cb 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 0b383b34d8..40590a220d 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 b91cbe699b..0a5379ee54 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;;