aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-09 03:35:20 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-25 00:33:36 +0200
commitee2197096fe75a63b4d92cb3a1bb05122c5c625b (patch)
tree3b40c06375a463625a2675b90e009fcb0b64a7d2 /pretyping/coercion.ml
parent054d2736c1c1b55cb7708ff0444af521cd0fe2ba (diff)
[location] [ast] Port module AST to CAst
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 acccfc125..a93653f32 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -79,8 +79,8 @@ let apply_pattern_coercion ?loc pat p =
List.fold_left
(fun pat (co,n) ->
let f i =
- if i<n then (Loc.tag ?loc @@ Glob_term.PatVar Anonymous) else pat in
- Loc.tag ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous))
+ if i<n then (CAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in
+ CAst.make ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous))
pat p
(* raise Not_found if no coercion found *)