diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 9fff64ae51..c3cdb361ba 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -17,6 +17,9 @@ open Util open Typeclasses_errors open Libobject open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration (*i*) let typeclasses_unique_solutions = ref false @@ -181,7 +184,7 @@ let subst_class (subst,cl) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst c = Mod_subst.subst_mps subst c and do_subst_gr gr = fst (subst_global subst gr) in - let do_subst_ctx = List.smartmap (map_constr do_subst) in + let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs, do_subst_ctx ctx in @@ -198,16 +201,15 @@ let discharge_class (_,cl) = let repl = Lib.replacement_context () in let rel_of_variable_context ctx = List.fold_right ( fun (decl,_) (ctx', subst) -> - let open Context.Named.Declaration in - let decl' = decl |> map_constr (substn_vars 1 subst) |> to_rel in - (decl' :: ctx', Context.Named.Declaration.get_id decl :: subst) + let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel in + (decl' :: ctx', NamedDecl.get_id decl :: subst) ) ctx ([], []) in let discharge_rel_context subst n rel = let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in let ctx, _ = List.fold_right (fun decl (ctx, k) -> - map_constr (substn_vars k subst) decl :: ctx, succ k + RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k ) rel ([], n) in ctx @@ -220,7 +222,7 @@ let discharge_class (_,cl) = let discharge_context ctx' subst (grs, ctx) = let grs' = let newgrs = List.map (fun decl -> - match decl |> get_type |> class_of_constr with + match decl |> RelDecl.get_type |> class_of_constr with | None -> None | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true)) ctx' |