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 ``` --- pretyping/typeclasses.ml | 86 ++++++++++++++++++++++++------------------------ 1 file changed, 43 insertions(+), 43 deletions(-) (limited to 'pretyping/typeclasses.ml') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 544fd3d17d..1541e96635 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -64,8 +64,8 @@ type typeclass = { (* The method implementations as projections. *) cl_projs : (Name.t * (direction * hint_info) option - * Constant.t option) list; - + * Constant.t option) list; + cl_strict : bool; cl_unique : bool; @@ -124,7 +124,7 @@ let class_of_constr env sigma c = try Some (dest_class_arity env sigma c) with e when CErrors.noncritical e -> None -let is_class_constr sigma c = +let is_class_constr sigma c = try let gr, u = Termops.global_of_constr sigma c in GlobRef.Map.mem gr !classes with Not_found -> false @@ -135,7 +135,7 @@ let rec is_class_type evd c = | Prod (_, _, t) -> is_class_type evd t | Cast (t, _, _) -> is_class_type evd t | _ -> is_class_constr evd c - + let is_class_evar evd evi = is_class_type evd evi.Evd.evar_concl @@ -160,7 +160,7 @@ let load_class cl = (** Build the subinstances hints. *) let check_instance env sigma c = - try + try let (evd, c) = resolve_one_typeclass env sigma (Retyping.get_type_of env sigma c) in not (Evd.has_undefined evd) @@ -168,8 +168,8 @@ let check_instance env sigma c = let build_subclasses ~check env sigma glob { hint_priority = pri } = let _id = Nametab.basename_of_global glob in - let _next_id = - let i = ref (-1) in + let _next_id = + let i = ref (-1) in (fun () -> incr i; Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in @@ -182,37 +182,37 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = match class_of_constr env sigma ty with | None -> [] | Some (rels, ((tc,u), args)) -> - let instapp = - Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels))) - in - let instapp = EConstr.Unsafe.to_constr instapp in - let projargs = Array.of_list (args @ [instapp]) in - let projs = List.map_filter - (fun (n, b, proj) -> - match b with - | None -> None - | Some (Backward, _) -> None - | Some (Forward, info) -> - let proj = Option.get proj in - let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in - let u = EConstr.EInstance.kind sigma u in - let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in - if check && check_instance env sigma (EConstr.of_constr body) then None - else - let newpri = - match pri, info.hint_priority with - | Some p, Some p' -> Some (p + p') - | Some p, None -> Some (p + 1) - | _, _ -> None - in + let instapp = + Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels))) + in + let instapp = EConstr.Unsafe.to_constr instapp in + let projargs = Array.of_list (args @ [instapp]) in + let projs = List.map_filter + (fun (n, b, proj) -> + match b with + | None -> None + | Some (Backward, _) -> None + | Some (Forward, info) -> + let proj = Option.get proj in + let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in + let u = EConstr.EInstance.kind sigma u in + let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in + if check && check_instance env sigma (EConstr.of_constr body) then None + else + let newpri = + match pri, info.hint_priority with + | Some p, Some p' -> Some (p + p') + | Some p, None -> Some (p + 1) + | _, _ -> None + in Some (GlobRef.ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs - in - let declare_proj hints (cref, info, body) = - let path' = cref :: path in - let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in - let rest = aux pri body ty path' in - hints @ (path', info, body) :: rest - in List.fold_left declare_proj [] projs + in + let declare_proj hints (cref, info, body) = + let path' = cref :: path in + let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in + let rest = aux pri body ty path' in + hints @ (path', info, body) :: rest + in List.fold_left declare_proj [] projs in let term = Constr.mkRef (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of @@ -249,10 +249,10 @@ let instance_constructor (cl,u) args = applist (mkIndU ind, pars)) | GlobRef.ConstRef cst -> let cst = cst, u in - let term = match args with - | [] -> None - | _ -> Some (List.last args) - in + let term = match args with + | [] -> None + | _ -> Some (List.last args) + in (term, applist (mkConstU cst, pars)) | _ -> assert false @@ -263,7 +263,7 @@ let cmap_elements c = GlobRef.Map.fold (fun k v acc -> v :: acc) c [] let instances_of c = try cmap_elements (GlobRef.Map.find c.cl_impl !instances) with Not_found -> [] -let all_instances () = +let all_instances () = GlobRef.Map.fold (fun k v acc -> GlobRef.Map.fold (fun k v acc -> v :: acc) v acc) !instances [] @@ -271,7 +271,7 @@ let all_instances () = let instances env sigma r = let cl = class_info env sigma r in instances_of cl -let is_class gr = +let is_class gr = GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes open Evar_kinds -- cgit v1.2.3