From b1d749e59444f86e40f897c41739168bb1b1b9b3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 25 Feb 2018 22:43:42 +0100
Subject: [located] Push inner locations in `reference` to a CAst.t node.

The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.

An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.

It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
---
 plugins/ssrmatching/ssrmatching.ml4 | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/ssrmatching')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 33b18001c9..6a1be9db06 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -131,8 +131,8 @@ let add_genarg tag pr =
 (** Constructors for cast type *)
 let dC t = CastConv t
 (** Constructors for constr_expr *)
-let isCVar   = function { CAst.v = CRef (Ident _, _) } -> true | _ -> false
-let destCVar = function { CAst.v = CRef (Ident (_, id), _) } -> id | _ ->
+let isCVar   = function { CAst.v = CRef ({CAst.v=Ident _},_) } -> true | _ -> false
+let destCVar = function { CAst.v = CRef ({CAst.v=Ident id},_) } -> id | _ ->
   CErrors.anomaly (str"not a CRef.")
 let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false
 let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c)
@@ -1012,8 +1012,8 @@ type pattern = Evd.evar_map * (constr, constr) ssrpattern
 let id_of_cpattern (_, (c1, c2), _) =
   let open CAst in
   match DAst.get c1, c2 with
-  | _, Some { v = CRef (Ident (_, x), _) } -> Some x
-  | _, Some { v = CAppExpl ((_, Ident (_, x), _), []) } -> Some x
+  | _, Some { v = CRef ({CAst.v=Ident x}, _) } -> Some x
+  | _, Some { v = CAppExpl ((_, {CAst.v=Ident x}, _), []) } -> Some x
   | GRef (VarRef x, _), None -> Some x
   | _ -> None
 let id_of_Cterm t = match id_of_cpattern t with
-- 
cgit v1.2.3