aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/coercion.ml')
-rw-r--r--pretyping/coercion.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0ec25d402..504d73cb8 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -82,8 +82,8 @@ let apply_pattern_coercion loc pat p =
pat p
(* raise Not_found if no coercion found *)
-let inh_pattern_coerce_to loc pat ind1 ind2 =
- let p = lookup_pattern_path_between (ind1,ind2) in
+let inh_pattern_coerce_to loc env pat ind1 ind2 =
+ let p = lookup_pattern_path_between env (ind1,ind2) in
apply_pattern_coercion loc pat p
(* Program coercions *)