aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/ssrparser.ml4
diff options
context:
space:
mode:
authorMaxime Dénès2018-03-10 10:04:56 +0100
committerMaxime Dénès2018-03-10 10:04:56 +0100
commit4d5c7243b4aea5b28358757e2d86c11334da6699 (patch)
treeade1ab73a9c2066302145bb3781a39b5d46b4513 /plugins/ssr/ssrparser.ml4
parent93a1c4786c9b17efdda025f754ad97376d61a9ba (diff)
parentb1d749e59444f86e40f897c41739168bb1b1b9b3 (diff)
Merge PR #6837: [located] Push inner locations in reference to a CAst.t node.
Diffstat (limited to 'plugins/ssr/ssrparser.ml4')
-rw-r--r--plugins/ssr/ssrparser.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 2f8b8cb02c..0d82a9f096 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1165,7 +1165,7 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar
END
let bvar_lname = let open CAst in function
- | { v = CRef (Ident (loc, id), _) } -> CAst.make ?loc @@ Name id
+ | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id
| { loc = loc } -> CAst.make ?loc Anonymous
let pr_ssrbinder prc _ _ (_, c) = prc c
@@ -1257,7 +1257,7 @@ END
let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd
let bvar_locid = function
- | { CAst.v = CRef (Ident (loc, id), _) } -> CAst.make ?loc id
+ | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id
| _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"")