aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/coercion.ml')
-rw-r--r--pretyping/coercion.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0b48654b6..0239a7e44 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -51,7 +51,7 @@ let apply_pattern_coercion loc pat p =
List.fold_left
(fun pat (co,n) ->
let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in
- Glob_term.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
+ Glob_term.PatCstr (loc, co, List.tabulate f (n+1), Anonymous))
pat p
(* raise Not_found if no coercion found *)