diff options
| author | Emilio Jesus Gallego Arias | 2019-10-30 23:36:37 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-31 14:17:53 +0100 |
| commit | 39f5e55e18afc15a9ed89508bcce4e3073c8b190 (patch) | |
| tree | faed8c8df2f2f0c0f1f9d7c4cda09494a65a3ea8 /vernac/classes.ml | |
| parent | 55646ce1aebb9e8d0147df785356cedc6805de3c (diff) | |
[classes] Untabify in preparation for next commit.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index cf668dfddb..42bc4e0d5c 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -47,7 +47,7 @@ let add_instance_hint inst path local info poly = in Flags.silently (fun () -> Hints.add_hints ~local [typeclasses_db] - (Hints.HintsResolveEntry + (Hints.HintsResolveEntry [info, poly, false, Hints.PathHints path, inst'])) () let is_local_for_hint i = @@ -287,7 +287,7 @@ let type_ctx_instance ~program_mode env sigma ctx inst subst = decl :: ctx -> let t' = substl subst (RelDecl.get_type decl) in let (sigma, c'), l = - match decl with + match decl with | LocalAssum _ -> interp_casted_constr_evars ~program_mode env sigma (List.hd l) t', List.tl l | LocalDef (_,b,_) -> (sigma, substl subst b), l in @@ -301,8 +301,8 @@ let id_of_class cl = match cl.cl_impl with | ConstRef kn -> Label.to_id @@ Constant.label kn | IndRef (kn,i) -> - let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in - mip.(0).Declarations.mind_typename + let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in + mip.(0).Declarations.mind_typename | _ -> assert false let instance_hook info global imps ?hook cst = @@ -495,9 +495,9 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri check_duplicate ?loc fs; let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in - let term, termtype = - do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in - Some term, termtype, sigma + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + Some term, termtype, sigma | Some (_, term) -> let sigma, def = interp_casted_constr_evars ~program_mode:true env' sigma term cty in |