From e81d7ccf99ac02476fb289042b7c653251160abf Mon Sep 17 00:00:00 2001 From: notin Date: Fri, 1 Sep 2006 11:04:44 +0000 Subject: Indentation + typo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9104 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/safe_typing.ml | 24 ++++++++++++------------ library/declare.ml | 24 ++++++++++++------------ library/lib.ml | 44 ++++++++++++++++++++++---------------------- library/libobject.ml | 2 +- theories/Lists/List.v | 4 ++-- toplevel/vernacentries.ml | 17 ++++++++--------- 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 -- cgit v1.2.3