aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.ml
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-08-26 13:18:02 +0200
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-08-26 13:18:02 +0200
commit69388fcd52b4a2aeefe843099c608d96defd1ce6 (patch)
treef31e4768b8db651eac5be33997c19417106e5bf9 /pretyping/typeclasses.ml
parent6cdcd498c4b425cad077f5bfaa453dc605b325a2 (diff)
CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,of}_rel_decl"
Diffstat (limited to 'pretyping/typeclasses.ml')
-rw-r--r--pretyping/typeclasses.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c3cdb361b..4c33a9c78 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -201,7 +201,7 @@ let discharge_class (_,cl) =
let repl = Lib.replacement_context () in
let rel_of_variable_context ctx = List.fold_right
( fun (decl,_) (ctx', subst) ->
- let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel in
+ let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in
(decl' :: ctx', NamedDecl.get_id decl :: subst)
) ctx ([], []) in
let discharge_rel_context subst n rel =