From d016f69818b30b75d186fb14f440b93b0518fc66 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 21 Nov 2019 15:38:39 +0100 Subject: [coq] Untabify the whole ML codebase. We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ``` --- library/coqlib.ml | 12 ++++---- library/coqlib.mli | 4 +-- library/global.ml | 4 +-- library/global.mli | 2 +- library/globnames.mli | 4 +-- library/goptions.ml | 32 ++++++++++---------- library/lib.ml | 10 +++--- library/libnames.ml | 2 +- library/libobject.ml | 12 ++++---- library/nametab.ml | 84 +++++++++++++++++++++++++-------------------------- library/nametab.mli | 2 +- 11 files changed, 84 insertions(+), 84 deletions(-) (limited to 'library') diff --git a/library/coqlib.ml b/library/coqlib.ml index 11d053624c..00ea8b8489 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -89,15 +89,15 @@ let gen_reference_in_modules locstr dirs s = match these with | [x] -> x | [] -> - anomaly ~label:locstr (str "cannot find " ++ str s ++ - str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ + anomaly ~label:locstr (str "cannot find " ++ str s ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma DirPath.print dirs ++ str ".") | l -> anomaly ~label:locstr - (str "ambiguous name " ++ str s ++ str " can represent " ++ - prlist_with_sep pr_comma - (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ - str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ + (str "ambiguous name " ++ str s ++ str " can represent " ++ + prlist_with_sep pr_comma + (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma DirPath.print dirs ++ str ".") (* For tactics/commands requiring vernacular libraries *) diff --git a/library/coqlib.mli b/library/coqlib.mli index ab8b18c4fb..10805416d1 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -210,9 +210,9 @@ val build_coq_f_equal2 : GlobRef.t delayed type coq_inversion_data = { inv_eq : GlobRef.t; (** : forall params, args -> Prop *) inv_ind : GlobRef.t; (** : forall params P (H : P params) args, eq params args - -> P args *) + -> P args *) inv_congr: GlobRef.t (** : forall params B (f:t->B) args, eq params args -> - f params = f args *) + f params = f args *) } val build_coq_inversion_eq_data : coq_inversion_data delayed diff --git a/library/global.ml b/library/global.ml index 98d3e9cb1f..d4262683bb 100644 --- a/library/global.ml +++ b/library/global.ml @@ -201,10 +201,10 @@ let is_type_in_type r = is_type_in_type (env ()) r let current_modpath () = Safe_typing.current_modpath (safe_env ()) -let current_dirpath () = +let current_dirpath () = Safe_typing.current_dirpath (safe_env ()) -let with_global f = +let with_global f = let (a, ctx) = f (env ()) (current_dirpath ()) in push_context_set false ctx; a diff --git a/library/global.mli b/library/global.mli index 0570ad0102..db0f87df7e 100644 --- a/library/global.mli +++ b/library/global.mli @@ -105,7 +105,7 @@ val lookup_named : variable -> Constr.named_declaration val lookup_constant : Constant.t -> Opaqueproof.opaque Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body -val lookup_pinductive : Constr.pinductive -> +val lookup_pinductive : Constr.pinductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body val lookup_mind : MutInd.t -> Declarations.mutual_inductive_body val lookup_module : ModPath.t -> Declarations.module_body diff --git a/library/globnames.mli b/library/globnames.mli index fc0de96e36..48cbb11b66 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -37,7 +37,7 @@ val subst_constructor : substitution -> constructor -> constructor val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t -(** This constr is not safe to be typechecked, universe polymorphism is not +(** This constr is not safe to be typechecked, universe polymorphism is not handled here: just use for printing *) val printable_constr_of_global : GlobRef.t -> constr @@ -60,6 +60,6 @@ module ExtRefOrdered : sig val hash : t -> int end -type global_reference_or_constr = +type global_reference_or_constr = | IsGlobal of GlobRef.t | IsConstr of constr diff --git a/library/goptions.ml b/library/goptions.ml index 0973944fb5..6e53bed349 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -52,12 +52,12 @@ type 'a table_of_A = { module MakeTable = functor (A : sig - type t + type t type key module Set : CSig.SetS with type elt = t val table : (string * key table_of_A) list ref val encode : Environ.env -> key -> t - val subst : substitution -> t -> t + val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name val title : string @@ -83,30 +83,30 @@ module MakeTable = | GOadd -> t := MySet.add p !t | GOrmv -> t := MySet.remove p !t in let load_options i o = if Int.equal i 1 then cache_options o in - let subst_options (subst,(f,p as obj)) = - let p' = A.subst subst p in - if p' == p then obj else - (f,p') - in + let subst_options (subst,(f,p as obj)) = + let p' = A.subst subst p in + if p' == p then obj else + (f,p') + in let inGo : option_mark * A.t -> obj = Libobject.declare_object {(Libobject.default_object nick) with Libobject.load_function = load_options; - Libobject.open_function = load_options; - Libobject.cache_function = cache_options; - Libobject.subst_function = subst_options; - Libobject.classify_function = (fun x -> Substitute x)} - in + Libobject.open_function = load_options; + Libobject.cache_function = cache_options; + Libobject.subst_function = subst_options; + Libobject.classify_function = (fun x -> Substitute x)} + in ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c)))) let print_table table_name printer table = Feedback.msg_notice (str table_name ++ - (hov 0 - (if MySet.is_empty table then str " None" ++ fnl () + (hov 0 + (if MySet.is_empty table then str " None" ++ fnl () else MySet.fold - (fun a b -> spc () ++ printer a ++ b) - table (mt ()) ++ str "." ++ fnl ()))) + (fun a b -> spc () ++ printer a ++ b) + table (mt ()) ++ str "." ++ fnl ()))) let table_of_A = { add = (fun env x -> add_option (A.encode env x)); diff --git a/library/lib.ml b/library/lib.ml index 630c860a61..c3c480aee4 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -52,7 +52,7 @@ let subst_atomic_objects subst seg = let subst_one = fun (id,obj as node) -> let obj' = subst_object (subst,obj) in if obj' == obj then node else - (id, obj') + (id, obj') in List.Smart.map subst_one seg @@ -296,15 +296,15 @@ let start_modtype = start_mod true None let error_still_opened string oname = let id = basename (fst oname) in - user_err + user_err (str "The " ++ str string ++ str " " ++ Id.print id ++ str " is still opened.") let end_mod is_type = let oname,fs = try match find_entry_p is_opening_node with | oname,OpenedModule (ty,_,_,fs) -> - if ty == is_type then oname, fs - else error_still_opened (module_kind ty) oname + if ty == is_type then oname, fs + else error_still_opened (module_kind ty) oname | oname,OpenedSection _ -> error_still_opened "section" oname | _ -> assert false with Not_found -> user_err (Pp.str "No opened modules.") @@ -359,7 +359,7 @@ let end_compilation_checks dir = match !lib_state.comp_name with | None -> anomaly (Pp.str "There should be a module name...") | Some m -> - if not (Names.DirPath.equal m dir) then anomaly + if not (Names.DirPath.equal m dir) then anomaly (str "The current open module has name" ++ spc () ++ DirPath.print m ++ spc () ++ str "and not" ++ spc () ++ DirPath.print m ++ str "."); in diff --git a/library/libnames.ml b/library/libnames.ml index 485f8837e8..126841c9a5 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -62,7 +62,7 @@ let parse_dir s = if n >= len then dirs else let pos = try - String.index_from s n '.' + String.index_from s n '.' with Not_found -> len in if Int.equal pos n then user_err Pp.(str @@ s ^ " is an invalid path."); diff --git a/library/libobject.ml b/library/libobject.ml index 932f065f73..a632a426fd 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -113,12 +113,12 @@ let declare_object_full odecl = and rebuild lobj = infun (odecl.rebuild_function (outfun lobj)) in Hashtbl.add cache_tab na { dyn_cache_function = cacher; - dyn_load_function = loader; + dyn_load_function = loader; dyn_open_function = opener; - dyn_subst_function = substituter; - dyn_classify_function = classifier; - dyn_discharge_function = discharge; - dyn_rebuild_function = rebuild }; + dyn_subst_function = substituter; + dyn_classify_function = classifier; + dyn_discharge_function = discharge; + dyn_rebuild_function = rebuild }; (infun,outfun) let declare_object odecl = fst (declare_object_full odecl) @@ -144,7 +144,7 @@ let load_object i ((_,lobj) as node) = let open_object i ((_,lobj) as node) = apply_dyn_fun (fun d -> d.dyn_open_function i node) lobj -let subst_object ((_,lobj) as node) = +let subst_object ((_,lobj) as node) = apply_dyn_fun (fun d -> d.dyn_subst_function node) lobj let classify_object lobj = diff --git a/library/nametab.ml b/library/nametab.ml index 8626ee1c59..283da5936c 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -128,7 +128,7 @@ struct (* Dictionaries of short names *) type nametree = { path : path_status; - map : nametree ModIdmap.t } + map : nametree ModIdmap.t } let mktree p m = { path=p; map=m } let empty_tree = mktree Nothing ModIdmap.empty @@ -149,34 +149,34 @@ struct let ptab = modify () empty_tree in ModIdmap.add modid ptab tree.map in - let this = + let this = if level <= 0 then - match tree.path with - | Absolute (n,_) -> - (* This is an absolute name, we must keep it - otherwise it may become unaccessible forever *) + match tree.path with + | Absolute (n,_) -> + (* This is an absolute name, we must keep it + otherwise it may become unaccessible forever *) warn_masking_absolute n; tree.path - | Nothing - | Relative _ -> Relative (uname,o) + | Nothing + | Relative _ -> Relative (uname,o) else tree.path - in - mktree this map + in + mktree this map | [] -> - match tree.path with - | Absolute (uname',o') -> - if E.equal o' o then begin - assert (U.equal uname uname'); - tree - (* we are putting the same thing for the second time :) *) - end - else - (* This is an absolute name, we must keep it otherwise it may - become unaccessible forever *) - (* But ours is also absolute! This is an error! *) - user_err Pp.(str @@ "Cannot mask the absolute name \"" + match tree.path with + | Absolute (uname',o') -> + if E.equal o' o then begin + assert (U.equal uname uname'); + tree + (* we are putting the same thing for the second time :) *) + end + else + (* This is an absolute name, we must keep it otherwise it may + become unaccessible forever *) + (* But ours is also absolute! This is an error! *) + user_err Pp.(str @@ "Cannot mask the absolute name \"" ^ U.to_string uname' ^ "\"!") - | Nothing - | Relative _ -> mktree (Absolute (uname,o)) tree.map + | Nothing + | Relative _ -> mktree (Absolute (uname,o)) tree.map let rec push_exactly uname o level tree = function | [] -> @@ -241,7 +241,7 @@ let user_name qid tab = let find uname tab = let id,l = U.repr uname in match search (Id.Map.find id tab) l with - Absolute (_,o) -> o + Absolute (_,o) -> o | _ -> raise Not_found let exists uname tab = @@ -260,9 +260,9 @@ let shortest_qualid ?loc ctx uname tab = | Absolute (u,_) | Relative (u,_) when U.equal u uname && not (is_empty && hidden) -> List.rev pos | _ -> - match dir with - [] -> raise Not_found - | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tree.map) + match dir with + [] -> raise Not_found + | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tree.map) in let ptab = Id.Map.find id tab in let found_dir = find_uname [] dir ptab in @@ -385,25 +385,25 @@ let the_univrevtab = Summary.ref ~name:"univrevtab" (UnivIdMap.empty : univrevta let push_xref visibility sp xref = match visibility with | Until _ -> - the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - the_globrevtab := Globrevtab.add xref sp !the_globrevtab + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + the_globrevtab := Globrevtab.add xref sp !the_globrevtab | _ -> - begin - if ExtRefTab.exists sp !the_ccitab then + begin + if ExtRefTab.exists sp !the_ccitab then let open GlobRef in - match ExtRefTab.find sp !the_ccitab with - | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) | - TrueGlobal( ConstructRef _) as xref -> - the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - | _ -> - the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - else - the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - end + match ExtRefTab.find sp !the_ccitab with + | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) | + TrueGlobal( ConstructRef _) as xref -> + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + | _ -> + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + else + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + end let push_cci visibility sp ref = push_xref visibility sp (TrueGlobal ref) - + (* This is for Syntactic Definitions *) let push_syndef visibility sp kn = push_xref visibility sp (SynDef kn) diff --git a/library/nametab.mli b/library/nametab.mli index 55458fe2c6..d603bd51e2 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -100,7 +100,7 @@ val error_global_not_found : qualid -> 'a object is loaded inside a module -- or - for a precise suffix, when the module containing (the module containing ...) the object is opened (imported) - + *) type visibility = Until of int | Exactly of int -- cgit v1.2.3