[ast] Adapt to Coq's #402 new generic AST node.

1 files changed, 242 insertions, 235 deletions

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index b5c54dc..1a9267a 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -112,9 +112,9 @@ let array_list_of_tl v =
 module Intset = Evar.Set
 
 type loc = Loc.t
-let dummy_loc = Loc.ghost
+
 let errorstrm msg = CErrors.user_err ~hdr:"ssreflect" msg
-let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg)
+let loc_error ?loc msg = CErrors.user_err ?loc ~hdr:msg (str msg)
 let anomaly s = CErrors.anomaly (str s)
 
 (* Compatibility with Coq 8.6 *)
@@ -131,7 +131,7 @@ let mkSsrRef name =
   try locate_reference (ssrqid name) with Not_found ->
   try locate_reference (ssrtopqid name) with Not_found ->
   CErrors.error "Small scale reflection library not loaded"
-let mkSsrRRef name = GRef (dummy_loc, mkSsrRef name,None), None
+let mkSsrRRef name = (CAst.make @@ GRef (mkSsrRef name,None)), None
 let mkSsrConst name env sigma =
   EConstr.fresh_global env sigma (mkSsrRef name)
 let pf_mkSsrConst name gl =
@@ -247,39 +247,39 @@ let add_genarg tag pr =
 let dC t = CastConv t
 
 (** Constructors for constr_expr *)
-let mkCProp loc = CSort (loc, GProp)
-let mkCType loc = CSort (loc, GType [])
-let mkCVar loc id = CRef (Ident (loc, id),None)
-let isCVar = function CRef (Ident _,_) -> true | _ -> false
-let destCVar = function CRef (Ident (_, id),_) -> id | _ ->
+let mkCProp loc = CAst.make ?loc @@ CSort GProp
+let mkCType loc = CAst.make ?loc @@ CSort (GType [])
+let mkCVar ?loc id = CAst.make ?loc @@ CRef (Ident (Loc.tag ?loc id), None)
+let isCVar = function { CAst.v = CRef (Ident _,_) } -> true | _ -> false
+let destCVar = function { CAst.v = CRef (Ident (_, id),_) } -> id | _ ->
   anomaly "not a CRef"
-let rec mkCHoles loc n =
-  if n <= 0 then [] else CHole (loc, None, IntroAnonymous, None) :: mkCHoles loc (n - 1)
-let mkCHole loc = CHole (loc, None, IntroAnonymous, None)
-let rec isCHoles = function CHole _ :: cl -> isCHoles cl | cl -> cl = []
-let mkCExplVar loc id n =
-   CAppExpl (loc, (None, Ident (loc, id), None), mkCHoles loc n)
-let mkCLambda loc name ty t = 
-   CLambdaN (loc, [[loc, name], Default Explicit, ty], t)
-let mkCLetIn loc name bo oty t = 
-   CLetIn (loc, (loc, name), bo, oty, t)
-let mkCArrow loc ty t =
-   CProdN (loc, [[dummy_loc,Anonymous], Default Explicit, ty], t)
-let mkCCast loc t ty = CCast (loc,t, dC ty)
+let rec mkCHoles ?loc n =
+  if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
+let mkCHole ?loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
+let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = []
+let mkCExplVar ?loc id n = CAst.make ?loc @@
+   CAppExpl ((None, Ident (loc, id), None), mkCHoles ?loc n)
+let mkCLambda ?loc name ty t =  CAst.make ?loc @@
+   CLambdaN ([[loc, name], Default Explicit, ty], t)
+let mkCLetIn ?loc name bo oty t =  CAst.make ?loc @@
+   CLetIn ((loc, name), bo, oty, t)
+let mkCArrow ?loc ty t = CAst.make ?loc @@
+   CProdN ([[Loc.tag Anonymous], Default Explicit, ty], t)
+let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty)
 (** Constructors for rawconstr *)
-let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None)
+let mkRHole = CAst.make @@ GHole (InternalHole, IntroAnonymous, None)
 let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else []
-let rec isRHoles = function GHole _ :: cl -> isRHoles cl | cl -> cl = []
-let mkRApp f args = if args = [] then f else GApp (dummy_loc, f, args)
-let mkRVar id = GRef (dummy_loc, VarRef id,None)
-let mkRltacVar id = GVar (dummy_loc, id)
-let mkRCast rc rt =  GCast (dummy_loc, rc, dC rt)
-let mkRType =  GSort (dummy_loc, GType [])
-let mkRProp =  GSort (dummy_loc, GProp)
-let mkRArrow rt1 rt2 = GProd (dummy_loc, Anonymous, Explicit, rt1, rt2)
-let mkRConstruct c = GRef (dummy_loc, ConstructRef c,None)
-let mkRInd mind = GRef (dummy_loc, IndRef mind,None)
-let mkRLambda n s t = GLambda (dummy_loc, n, Explicit, s, t)
+let rec isRHoles = function { CAst.v = GHole _ } :: cl -> isRHoles cl | cl -> cl = []
+let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args)
+let mkRVar id = CAst.make @@ GRef (VarRef id,None)
+let mkRltacVar id = CAst.make @@ GVar (id)
+let mkRCast rc rt =  CAst.make @@ GCast (rc, dC rt)
+let mkRType =  CAst.make @@ GSort (GType [])
+let mkRProp =  CAst.make @@ GSort (GProp)
+let mkRArrow rt1 rt2 = CAst.make @@ GProd (Anonymous, Explicit, rt1, rt2)
+let mkRConstruct c = CAst.make @@ GRef (ConstructRef c,None)
+let mkRInd mind = CAst.make @@ GRef (IndRef mind,None)
+let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t)
 
 (** Constructors for constr *)
 let pf_e_type_of gl t =
@@ -667,13 +667,13 @@ let internal_names = ref []
 let add_internal_name pt = internal_names := pt :: !internal_names
 let is_internal_name s = List.exists (fun p -> p s) !internal_names
 
-let ssr_id_of_string loc s =
+let ssr_id_of_string ?loc s =
   if is_ssr_reserved s && is_ssr_loaded () then begin
     if !ssr_reserved_ids then
-      loc_error loc ("The identifier " ^ s ^ " is reserved.")
+      loc_error ?loc ("The identifier " ^ s ^ " is reserved.")
     else if is_internal_name s then
-      msg_warning (str ("Conflict between " ^ s ^ " and ssreflect internal names."))
-    else msg_warning (str (
+      msg_warning ?loc (str ("Conflict between " ^ s ^ " and ssreflect internal names."))
+    else msg_warning ?loc (str (
      "The name " ^ s ^ " fits the _xxx_ format used for anonymous variables.\n"
   ^ "Scripts with explicit references to anonymous variables are fragile."))
     end; id_of_string s
@@ -684,7 +684,7 @@ let (!@) = Pcoq.to_coqloc
 
 GEXTEND Gram 
   GLOBAL: Prim.ident;
-  Prim.ident: [[ s = IDENT; ssr_null_entry -> ssr_id_of_string !@loc s ]];
+  Prim.ident: [[ s = IDENT; ssr_null_entry -> ssr_id_of_string ~loc:!@loc s ]];
 END
 
 let mk_internal_id s =
@@ -1076,8 +1076,8 @@ let set_pr_ssrtac name prec afmt =
     | ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in
   let tacname = ssrtac_name name in ()
 
-let ssrtac_atom loc name args = TacML (loc, ssrtac_entry name 0, args)
-let ssrtac_expr = ssrtac_atom
+let ssrtac_atom ?loc name args = TacML (Loc.tag ?loc (ssrtac_entry name 0, args))
+let ssrtac_expr ?loc name args = ssrtac_atom ?loc name args
 
 
 let ssrevaltac ist gtac =
@@ -1232,17 +1232,17 @@ END
 
 type raw_glob_search_about_item =
   | RGlobSearchSubPattern of constr_expr
-  | RGlobSearchString of Loc.t * string * string option
+  | RGlobSearchString of (string * string option) Loc.located
 
 let pr_search_item = function
-  | RGlobSearchString (_,s,_) -> str s
+  | RGlobSearchString (_,(s,_)) -> str s
   | RGlobSearchSubPattern p -> pr_constr_expr p
 
 let wit_ssr_searchitem = add_genarg "ssr_searchitem" pr_search_item
 
-let interp_search_notation loc s opt_scope =
+let interp_search_notation ?loc s opt_scope =
   try
-    let interp = Notation.interp_notation_as_global_reference loc in
+    let interp = Notation.interp_notation_as_global_reference ?loc in
     let ref = interp (fun _ -> true) s opt_scope in
     Search.GlobSearchSubPattern (Pattern.PRef ref)
   with _ ->
@@ -1252,7 +1252,7 @@ let interp_search_notation loc s opt_scope =
         let ambig = "This string refers to a complex or ambiguous notation." in
         str ambig ++ str "\nTry searching with one of\n" ++ ntns
       with _ -> str "This string is not part of an identifier or notation." in
-    CErrors.user_err ~loc ~hdr:"interp_search_notation" diagnosis
+    CErrors.user_err ?loc ~hdr:"interp_search_notation" diagnosis
 
 let pr_ssr_search_item _ _ _ = pr_search_item
 
@@ -1262,8 +1262,8 @@ let is_ident s = try CLexer.check_ident s; true with _ -> false
 
 let is_ident_part s = is_ident ("H" ^ s)
 
-let interp_search_notation loc tag okey =
-  let err msg = CErrors.user_err ~loc ~hdr:"interp_search_notation" msg in
+let interp_search_notation ?loc tag okey =
+  let err msg = CErrors.user_err ?loc ~hdr:"interp_search_notation" msg in
   let mk_pntn s for_key =
     let n = String.length s in
     let s' = Bytes.make (n + 2) ' ' in
@@ -1290,7 +1290,7 @@ let interp_search_notation loc tag okey =
   let generator, pr_tag_sc =
     let ign _ = mt () in match okey with
   | Some key ->
-    let sc = Notation.find_delimiters_scope loc key in
+    let sc = Notation.find_delimiters_scope ?loc key in
     let pr_sc s_in = str s_in ++ spc() ++ str sc ++ pr_comma() in
     Notation.pr_scope ign sc, pr_sc
   | None -> Notation.pr_scopes ign, ign in
@@ -1335,9 +1335,9 @@ let interp_search_notation loc tag okey =
     let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in
     err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in
   let (nvars, body), ((_, pat), osc) = match !scs with
-  | [sc] -> Notation.interp_notation loc ntn (None, [sc])
+  | [sc] -> Notation.interp_notation ?loc ntn (None, [sc])
   | scs' ->
-    try Notation.interp_notation loc ntn (None, []) with _ ->
+    try Notation.interp_notation ?loc ntn (None, []) with _ ->
     let e = pr_ntn ntn ++ spc() ++ str "is defined " ++ pr_scs scs' in
     err (hov 4 (str "ambiguous: " ++ pr_tag_sc "in" ++ e)) in
   let sc = Option.default "" osc in
@@ -1345,7 +1345,7 @@ let interp_search_notation loc tag okey =
     let m_sc =
       if osc <> None then str "In " ++ str sc ++ pr_comma() else mt() in
     let ntn_pat = trim_ntn (mk_pntn pat false) in
-    let rbody = glob_constr_of_notation_constr loc body in
+    let rbody = glob_constr_of_notation_constr ?loc body in
     let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in
     let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in
     msgnl (hov 0 m) in
@@ -1357,16 +1357,16 @@ let interp_search_notation loc tag okey =
     err (pr_ntn ntn ++ str " is an n-ary notation");
   let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in
   let rec sub () = function
-  | NVar x when List.mem_assoc x nvars -> GPatVar (loc, (false, x))
+  | NVar x when List.mem_assoc x nvars -> CAst.make ?loc @@ GPatVar (false, x)
   | c ->
-    glob_constr_of_notation_constr_with_binders loc (fun _ x -> (), x) sub () c in
+    glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), x) sub () c in
   let _, npat = Patternops.pattern_of_glob_constr (sub () body) in
   Search.GlobSearchSubPattern npat
 
 ARGUMENT EXTEND ssr_search_item TYPED AS ssr_searchitem
   PRINTED BY pr_ssr_search_item
-  | [ string(s) ] -> [ RGlobSearchString (loc,s,None) ]
-  | [ string(s) "%" preident(key) ] -> [ RGlobSearchString (loc,s,Some key) ]
+  | [ string(s) ] -> [ RGlobSearchString (Loc.tag ~loc (s,None)) ]
+  | [ string(s) "%" preident(key) ] -> [ RGlobSearchString (Loc.tag ~loc (s,Some key)) ]
   | [ constr_pattern(p) ] -> [ RGlobSearchSubPattern p ]
 END
 
@@ -1446,9 +1446,9 @@ let rec interp_search_about args accu = match args with
 
 let interp_search_arg arg =
   let arg = List.map (fun (x,arg) -> x, match arg with
-  | RGlobSearchString (loc,s,key) ->
+  | RGlobSearchString (loc,(s,key)) ->
       if is_ident_part s then Search.GlobSearchString s else
-      interp_search_notation loc s key
+      interp_search_notation ?loc s key
   | RGlobSearchSubPattern p ->
       try
         let intern = Constrintern.intern_constr_pattern in 
@@ -1488,7 +1488,7 @@ let interp_modloc mr =
   let interp_mod (_, mr) =
     let (loc, qid) = qualid_of_reference mr in
     try Nametab.full_name_module qid with Not_found ->
-    CErrors.user_err ~loc ~hdr:"interp_modloc" (str "No Module " ++ pr_qualid qid) in
+    CErrors.user_err ?loc ~hdr:"interp_modloc" (str "No Module " ++ pr_qualid qid) in
   let mr_out, mr_in = List.partition fst mr in
   let interp_bmod b = function
   | [] -> fun _ _ _ -> true
@@ -1542,43 +1542,43 @@ END
 
 let no_ct = None, None and no_rt = None in 
 let aliasvar = function
-  | [_, [CPatAlias (loc, _, id)]] -> Some (loc,Name id)
+  | [_, [{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id)
   | _ -> None in
 let mk_cnotype mp = aliasvar mp, None in
 let mk_ctype mp t = aliasvar mp, Some t in
 let mk_rtype t = Some t in
-let mk_dthen loc (mp, ct, rt) c = (loc, mp, c), ct, rt in
-let mk_let loc rt ct mp c1 =
-  CCases (loc, LetPatternStyle, rt, ct, [loc, mp, c1]) in
+let mk_dthen ?loc (mp, ct, rt) c = (Loc.tag ?loc (mp, c)), ct, rt in
+let mk_let ?loc rt ct mp c1 =
+  CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [Loc.tag ?loc (mp, c1)]) in
 let mk_pat c (na, t) = (c, na, t) in
 GEXTEND Gram
   GLOBAL: binder_constr;
   ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> mk_rtype t ]];
-  ssr_mpat: [[ p = pattern -> [!@loc, [p]] ]];
+  ssr_mpat: [[ p = pattern -> [Loc.tag ~loc:!@loc [p]] ]];
   ssr_dpat: [
     [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> mp, mk_ctype mp t, rt
     | mp = ssr_mpat; rt = ssr_rtype -> mp, mk_cnotype mp, rt
     | mp = ssr_mpat -> mp, no_ct, no_rt
   ] ];
-  ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen !@loc dp c ]];
-  ssr_elsepat: [[ "else" -> [!@loc, [CPatAtom (!@loc, None)]] ]];
-  ssr_else: [[ mp = ssr_elsepat; c = lconstr -> !@loc, mp, c ]];
+  ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]];
+  ssr_elsepat: [[ "else" -> [Loc.tag ~loc:!@loc [CAst.make ~loc:!@loc @@ CPatAtom None]] ]];
+  ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]];
   binder_constr: [
     [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
-      let b1, ct, rt = db1 in CCases (!@loc, MatchStyle, rt, [mk_pat c ct], [b1; b2])
+      let b1, ct, rt = db1 in CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2])
     | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
       let b1, ct, rt = db1 in 
       let b1, b2 = 
-        let (l1, p1, r1), (l2, p2, r2) = b1, b2 in (l1, p1, r2), (l2, p2, r1) in
-      CCases (!@loc, MatchStyle, rt, [mk_pat c ct], [b1; b2])
+        let (l1, (p1, r1)), (l2, (p2, r2)) = b1, b2 in (l1, (p1, r2)), (l2, (p2, r1)) in
+      CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2])
     | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr ->
-      mk_let (!@loc) no_rt [mk_pat c no_ct] mp c1
+      mk_let ~loc:!@loc no_rt [mk_pat c no_ct] mp c1
     | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr;
       rt = ssr_rtype; "in"; c1 = lconstr ->
-      mk_let (!@loc) rt [mk_pat c (mk_cnotype mp)] mp c1
+      mk_let ~loc:!@loc rt [mk_pat c (mk_cnotype mp)] mp c1
     | "let"; ":"; mp = ssr_mpat; "in"; t = pattern; ":="; c = lconstr;
       rt = ssr_rtype; "in"; c1 = lconstr ->
-      mk_let (!@loc) rt [mk_pat c (mk_ctype mp t)] mp c1
+      mk_let ~loc:!@loc rt [mk_pat c (mk_ctype mp t)] mp c1
   ] ];
 END
 
@@ -1586,7 +1586,7 @@ GEXTEND Gram
   GLOBAL: closed_binder;
   closed_binder: [
     [ ["of" | "&"]; c = operconstr LEVEL "99" ->
-      [CLocalAssum ([!@loc, Anonymous], Default Explicit, c)]
+      [CLocalAssum ([Loc.tag ~loc:!@loc Anonymous], Default Explicit, c)]
   ] ];
 END
 (* }}} *)
@@ -1603,7 +1603,7 @@ END
 
 GEXTEND Gram
   GLOBAL: tactic_expr;
-  ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> !@loc, Tacexp tac ]];
+  ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> Loc.tag ~loc:!@loc (Tacexp tac) ]];
   tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> TacArg arg ]];
 END
 
@@ -1621,7 +1621,7 @@ let donetac gl =
     try Nametab.locate_tactic (qualid_of_ident (id_of_string "done"))
     with Not_found -> try Nametab.locate_tactic (ssrqid "done")
     with Not_found -> CErrors.error "The ssreflect library was not loaded" in
-  let tacexpr = dummy_loc, Tacexpr.Reference (ArgArg (dummy_loc, tacname)) in
+  let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
   Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
 
 let prof_donetac = mk_profiler "donetac";;
@@ -1632,7 +1632,7 @@ let ssrautoprop gl =
     let tacname = 
       try Nametab.locate_tactic (qualid_of_ident (id_of_string "ssrautoprop"))
       with Not_found -> Nametab.locate_tactic (ssrqid "ssrautoprop") in
-    let tacexpr = dummy_loc, Tacexpr.Reference (ArgArg (dummy_loc, tacname)) in
+    let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
     Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
   with Not_found -> Proofview.V82.of_tactic (Auto.full_trivial []) gl
 
@@ -1743,9 +1743,9 @@ let gen_tclarg tac = TacGeneric (in_gen (rawwit wit_ssrtclarg) tac)
 GEXTEND Gram
   GLOBAL: tactic tactic_mode;
   tactic: [
-    [ "+"; tac = ssrtclarg -> ssrtac_expr !@loc "tclplus" [gen_tclarg tac]
-    | "-"; tac = ssrtclarg -> ssrtac_expr !@loc "tclminus" [gen_tclarg tac]
-    | "*"; tac = ssrtclarg -> ssrtac_expr !@loc "tclstar" [gen_tclarg tac] 
+    [ "+"; tac = ssrtclarg -> ssrtac_expr ~loc:!@loc "tclplus" [gen_tclarg tac]
+    | "-"; tac = ssrtclarg -> ssrtac_expr ~loc:!@loc "tclminus" [gen_tclarg tac]
+    | "*"; tac = ssrtclarg -> ssrtac_expr ~loc:!@loc "tclstar" [gen_tclarg tac] 
     ] ];
   tactic_mode: [
     [ "+"; tac = G_vernac.query_command -> tac None
@@ -1785,7 +1785,7 @@ END
 (* idents that match global/section constants, since this would lead to    *)
 (* fragile Ltac scripts.                                                   *)
 
-type ssrhyp = SsrHyp of loc * identifier
+type ssrhyp = SsrHyp of identifier Loc.located
 
 let hyp_id (SsrHyp (_, id)) = id
 let pr_hyp (SsrHyp (_, id)) = pr_id id
@@ -1793,23 +1793,23 @@ let pr_ssrhyp _ _ _ = pr_hyp
 
 let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp
 
-let hyp_err loc msg id =
-  CErrors.user_err ~loc ~hdr:"ssrhyp" (str msg ++ pr_id id)
+let hyp_err ?loc msg id =
+  CErrors.user_err ?loc ~hdr:"ssrhyp" (str msg ++ pr_id id)
 
 let intern_hyp ist (SsrHyp (loc, id) as hyp) =
   let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) (loc, id)) in
   if not_section_id id then hyp else
-  hyp_err loc "Can't clear section hypothesis " id
+  hyp_err ?loc "Can't clear section hypothesis " id
 
 let interp_hyp ist gl (SsrHyp (loc, id)) =
   let s, id' = interp_wit wit_var ist gl (loc, id) in
   if not_section_id id' then s, SsrHyp (loc, id') else
-  hyp_err loc "Can't clear section hypothesis " id'
+  hyp_err ?loc "Can't clear section hypothesis " id'
 
 ARGUMENT EXTEND ssrhyp TYPED AS ssrhyprep PRINTED BY pr_ssrhyp
                        INTERPRETED BY interp_hyp
                        GLOBALIZED BY intern_hyp
-  | [ ident(id) ] -> [ SsrHyp (loc, id) ]
+  | [ ident(id) ] -> [ SsrHyp (Loc.tag ~loc id) ]
 END
 
 type ssrhyp_or_id = Hyp of ssrhyp | Id of ssrhyp
@@ -1836,12 +1836,12 @@ let interp_ssrhoi ist gl = function
 ARGUMENT EXTEND ssrhoi_hyp TYPED AS ssrhoirep PRINTED BY pr_ssrhoi
                        INTERPRETED BY interp_ssrhoi
                        GLOBALIZED BY intern_ssrhoi
-  | [ ident(id) ] -> [ Hyp (SsrHyp(loc, id)) ]
+  | [ ident(id) ] -> [ Hyp (SsrHyp(Loc.tag ~loc id)) ]
 END
 ARGUMENT EXTEND ssrhoi_id TYPED AS ssrhoirep PRINTED BY pr_ssrhoi
                        INTERPRETED BY interp_ssrhoi
                        GLOBALIZED BY intern_ssrhoi
-  | [ ident(id) ] -> [ Id (SsrHyp(loc, id)) ]
+  | [ ident(id) ] -> [ Id (SsrHyp(Loc.tag ~loc id)) ]
 END
 
 type ssrhyps = ssrhyp list
@@ -1852,7 +1852,7 @@ let hyps_ids = List.map hyp_id
 
 let rec check_hyps_uniq ids = function
   | SsrHyp (loc, id) :: _ when List.mem id ids ->
-    hyp_err loc "Duplicate assumption " id
+    hyp_err ?loc "Duplicate assumption " id
   | SsrHyp (_, id) :: hyps -> check_hyps_uniq (id :: ids) hyps
   | [] -> ()
 
@@ -2121,7 +2121,7 @@ let abs_wgen keep_let ist f gen (gl,args,c) =
   let c = EConstr.Unsafe.to_constr c in
   let evar_closed t p =
     if occur_existential sigma(*XXX*) t then
-      CErrors.user_err ~loc:(loc_of_cpattern p) ~hdr:"ssreflect"
+      CErrors.user_err ?loc:(loc_of_cpattern p) ~hdr:"ssreflect"
         (pr_constr_pat (EConstr.Unsafe.to_constr t) ++
         str" contains holes and matches no subterm of the goal") in
   match gen with
@@ -2160,7 +2160,7 @@ let abs_wgen keep_let ist f gen (gl,args,c) =
 let clr_of_wgen gen clrs = match gen with
   | clr, Some ((x, _), None) ->
      let x = hoi_id x in
-     cleartac clr :: cleartac [SsrHyp(Loc.ghost,x)] :: clrs
+     cleartac clr :: cleartac [SsrHyp(Loc.tag x)] :: clrs
   | clr, _ -> cleartac clr :: clrs
     
 let tclCLAUSES ist tac (gens, clseq) gl =
@@ -2253,9 +2253,9 @@ let pr_ssrindex _ _ _ = pr_index
 let noindex = ArgArg 0
 let allocc = Some(false,[])
 
-let check_index loc i =
-  if i > 0 then i else loc_error loc "Index not positive"
-let mk_index loc = function ArgArg i -> ArgArg (check_index loc i) | iv -> iv
+let check_index ?loc i =
+  if i > 0 then i else loc_error ?loc "Index not positive"
+let mk_index ?loc = function ArgArg i -> ArgArg (check_index ?loc i) | iv -> iv
 
 let interp_index ist gl idx =
   Tacmach.project gl, 
@@ -2277,12 +2277,12 @@ let interp_index ist gl idx =
           end
         | None -> raise Not_found
         end end
-    with _ -> loc_error loc "Index not a number" in
-    ArgArg (check_index loc i)
+    with _ -> loc_error ?loc "Index not a number" in
+    ArgArg (check_index ?loc i)
 
 ARGUMENT EXTEND ssrindex TYPED AS ssrindex PRINTED BY pr_ssrindex
   INTERPRETED BY interp_index
-| [ int_or_var(i) ] -> [ mk_index loc i ]
+| [ int_or_var(i) ] -> [ mk_index ~loc i ]
 END
 
 (** Occurrence switch *)
@@ -2308,7 +2308,7 @@ let pr_ssrocc _ _ _ = pr_occ
 
 ARGUMENT EXTEND ssrocc TYPED AS (bool * int list) option PRINTED BY pr_ssrocc
 | [ natural(n) natural_list(occ) ] -> [
-     Some (false, List.map (check_index loc) (n::occ)) ]
+     Some (false, List.map (check_index ~loc) (n::occ)) ]
 | [ "-" natural_list(occ) ]     -> [ Some (true, occ) ]
 | [ "+" natural_list(occ) ]     -> [ Some (false, occ) ]
 END
@@ -2348,18 +2348,18 @@ END
 
 (* View hints *)
 
-let rec isCxHoles = function (CHole _, None) :: ch -> isCxHoles ch | _ -> false
+let rec isCxHoles = function ({ CAst.v = CHole _ }, None) :: ch -> isCxHoles ch | _ -> false
 
-let pr_raw_ssrhintref prc _ _ = function
-  | CAppExpl (_, (None, r,x), args) when isCHoles args ->
-    prc (CRef (r,x)) ++ str "|" ++ int (List.length args)
-  | CApp (_, (_, CRef _), _) as c -> prc c
-  | CApp (_, (_, c), args) when isCxHoles args ->
+let pr_raw_ssrhintref prc _ _ = let open CAst in function
+  | { v = CAppExpl ((None, r,x), args) } when isCHoles args ->
+    prc (CAst.make @@ CRef (r,x)) ++ str "|" ++ int (List.length args)
+  | { v = CApp ((_, { v = CRef _ }), _) } as c -> prc c
+  | { v = CApp ((_, c), args) } when isCxHoles args ->
     prc c ++ str "|" ++ int (List.length args)
   | c -> prc c
 
-let pr_rawhintref = function
-  | GApp (_, f, args) when isRHoles args ->
+let pr_rawhintref = let open CAst in function
+  | { v = GApp (f, args) } when isRHoles args ->
     pr_glob_constr f ++ str "|" ++ int (List.length args)
   | c -> pr_glob_constr c
 
@@ -2367,16 +2367,16 @@ let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c
 
 let pr_ssrhintref prc _ _ = prc
 
-let mkhintref loc c n = match c with
-  | CRef (r,x) -> CAppExpl (loc, (None, r, x), mkCHoles loc n)
-  | _ -> mkAppC (c, mkCHoles loc n)
+let mkhintref ?loc c n = match c.CAst.v with
+  | CRef (r,x) -> CAst.make ?loc @@ CAppExpl ((None, r, x), mkCHoles ?loc n)
+  | _ -> mkAppC (c, mkCHoles ?loc n)
 
 ARGUMENT EXTEND ssrhintref
                              PRINTED BY pr_ssrhintref
     RAW_TYPED AS constr  RAW_PRINTED BY pr_raw_ssrhintref
    GLOB_TYPED AS constr GLOB_PRINTED BY pr_glob_ssrhintref
   | [ constr(c) ] -> [ c ]
-  | [ constr(c) "|" natural(n) ] -> [ mkhintref loc c n ]
+  | [ constr(c) "|" natural(n) ] -> [ mkhintref ~loc c n ]
 END
 
 (* View purpose *)
@@ -2488,9 +2488,10 @@ let view_error s gv =
   errorstrm (str ("Cannot " ^ s ^ " view ") ++ pr_term gv)
 
 let interp_view ist si env sigma gv rid =
+  let open CAst in
   match intern_term ist sigma env gv with
-  | GApp (loc, GHole _, rargs) ->
-    let rv = GApp (loc, rid, rargs) in
+  | { v = GApp ( { v = GHole _ } , rargs); loc } ->
+    let rv = make ?loc @@ GApp (rid, rargs) in
     snd (interp_open_constr ist (re_sig si sigma) (rv, None))
   | rv ->
   let interp rc rargs =
@@ -2599,13 +2600,13 @@ let intern_ipat ist ipat =
 let intern_ipats ist = List.map (intern_ipat ist)
 
 let interp_introid ist gl id =
- try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (dummy_loc, id))))))
- with _ -> snd(snd (interp_intro_pattern ist gl (dummy_loc,IntroNaming (IntroIdentifier id))))
+ try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id))))))
+ with _ -> snd(snd (interp_intro_pattern ist gl (Loc.tag @@ IntroNaming (IntroIdentifier id))))
 
 let rec add_intro_pattern_hyps (loc, ipat) hyps = match ipat with
   | IntroNaming (IntroIdentifier id) ->
     if not_section_id id then SsrHyp (loc, id) :: hyps else
-    hyp_err loc "Can't delete section hypothesis " id
+    hyp_err ?loc "Can't delete section hypothesis " id
   | IntroAction IntroWildcard -> hyps
   | IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) ->
     List.fold_right (List.fold_right add_intro_pattern_hyps) iorpat hyps
@@ -2667,7 +2668,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats
       | Some clr, _ -> [IpatSimpl (clr, Nop); IpatRw (allocc, R2L)]]
   | [ ssrdocc(occ) ] -> [ match occ with
       | Some cl, _ -> check_hyps_uniq [] cl; [IpatSimpl (cl, Nop)]
-      | _ -> loc_error loc "Only identifiers are allowed here"]
+      | _ -> loc_error ~loc "Only identifiers are allowed here"]
   | [ "->" ] -> [ [IpatRw (allocc, L2R)] ]
   | [ "<-" ] -> [ [IpatRw (allocc, R2L)] ]
   | [ "-" ] -> [ [IpatNoop] ]
@@ -2759,7 +2760,7 @@ let check_ssrhpats loc w_binders ipats =
   ((clr, ipat), binders), simpl
 
 let single loc =
-  function [x] -> x | _ -> loc_error loc "Only one intro pattern is allowed"
+  function [x] -> x | _ -> loc_error ?loc "Only one intro pattern is allowed"
 
 let pr_hpats (((clr, ipat), binders), simpl) =
    pr_clear mt clr ++ pr_ipats ipat ++ pr_ipats binders ++ pr_ipats simpl
@@ -2989,7 +2990,7 @@ let introstac, tclEQINTROS =
       let ren_clr, ren = 
         List.split (List.map (fun x -> let x = hyp_id x in
           let x' = mk_anon_id (string_of_id x) gl in
-          SsrHyp (dummy_loc, x'), (x, x')) clr) in
+          (SsrHyp (Loc.tag x')), (x, x')) clr) in
       let () = to_clr := ren_clr in
       Proofview.V82.of_tactic (rename_hyp ren) gl 
     else
@@ -3016,7 +3017,7 @@ let introstac, tclEQINTROS =
               tclTHEN
                 (!move_top_with_view false top_id (false,v) ist)
                 (fun gl -> 
-                  rename true to_clr rest [SsrHyp (dummy_loc, !top_id)]gl)
+                  rename true to_clr rest [SsrHyp (Loc.tag !top_id)]gl)
             | _ -> k, !move_top_with_view true (ref top_id) (true,v) ist
   and tclIORPAT ?ist k tac = function
     | [[]] -> tac
@@ -3081,14 +3082,14 @@ TACTIC EXTEND ssrtclintros
 END
 set_pr_ssrtac "tclintros" 0 [ArgSsr "introsarg"]
 
-let tclintros_expr loc tac ipats =
+let tclintros_expr ?loc tac ipats =
   let args = [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in
-  ssrtac_expr loc "tclintros" args
+  ssrtac_expr ?loc "tclintros" args
 
 GEXTEND Gram
   GLOBAL: tactic_expr;
   tactic_expr: LEVEL "1" [ RIGHTA
-    [ tac = tactic_expr; intros = ssrintros_ne -> tclintros_expr !@loc tac intros
+    [ tac = tactic_expr; intros = ssrintros_ne -> tclintros_expr ~loc:!@loc tac intros
     ] ];
 END
 (* }}} *)
@@ -3128,7 +3129,7 @@ let tclDO n tac =
         let _, info = CErrors.push e in
         let e' = CErrors.UserError (l, prefix i ++ s) in
         Util.iraise (e', info)
-    | Ploc.Exc(loc, CErrors.UserError (l, s))  -> 
+    | Ploc.Exc(loc, CErrors.UserError (l, s))  ->
         raise (Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
   let rec loop i gl =
     if i = n then tac_err_at i gl else
@@ -3167,9 +3168,9 @@ TACTIC EXTEND ssrtcldo
 END
 set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"]
 
-let ssrdotac_expr loc n m tac clauses =
+let ssrdotac_expr ?loc n m tac clauses =
   let arg = ((n, m), tac), clauses in
-  ssrtac_expr loc "tcldo" [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrdoarg) arg)]
+  ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrdoarg) arg)]
 
 GEXTEND Gram
   GLOBAL: tactic_expr;
@@ -3179,12 +3180,12 @@ GEXTEND Gram
   ] ];
   tactic_expr: LEVEL "3" [ RIGHTA
     [ IDENT "do"; m = ssrmmod; tac = ssrdotac; clauses = ssrclauses ->
-      ssrdotac_expr !@loc noindex m tac clauses
+      ssrdotac_expr ~loc:!@loc noindex m tac clauses
     | IDENT "do"; tac = ssrortacarg; clauses = ssrclauses ->
-      ssrdotac_expr !@loc noindex Once tac clauses
+      ssrdotac_expr ~loc:!@loc noindex Once tac clauses
     | IDENT "do"; n = int_or_var; m = ssrmmod;
                   tac = ssrdotac; clauses = ssrclauses ->
-      ssrdotac_expr !@loc (mk_index !@loc n) m tac clauses
+      ssrdotac_expr ~loc:!@loc (mk_index ~loc:!@loc n) m tac clauses
     ] ];
 END
 (* }}} *)
@@ -3225,17 +3226,17 @@ let swaptacarg (loc, b) = (b, []), Some (TacId [])
 
 let check_seqtacarg dir arg = match snd arg, dir with
   | ((true, []), Some (TacAtom (loc, _))), L2R ->
-    loc_error loc "expected \"last\""
+    loc_error ?loc "expected \"last\""
   | ((false, []), Some (TacAtom (loc, _))), R2L ->
-    loc_error loc "expected \"first\""
+    loc_error ?loc "expected \"first\""
   | _, _ -> arg
 
 let ssrorelse = Gram.entry_create "ssrorelse"
 GEXTEND Gram
   GLOBAL: ssrorelse ssrseqarg;
   ssrseqidx: [
-    [ test_ssrseqvar; id = Prim.ident -> ArgVar (!@loc, id)
-    | n = Prim.natural -> ArgArg (check_index !@loc n)
+    [ test_ssrseqvar; id = Prim.ident -> ArgVar (Loc.tag ~loc:!@loc id)
+    | n = Prim.natural -> ArgArg (check_index ~loc:!@loc n)
     ] ];
   ssrswap: [[ IDENT "first" -> !@loc, true | IDENT "last" -> !@loc, false ]];
   ssrorelse: [[ "||"; tac = tactic_expr LEVEL "2" -> tac ]];
@@ -3332,16 +3333,16 @@ TACTIC EXTEND ssrtclseq
 END
 set_pr_ssrtac "tclseq" 5 [ArgSsr "tclarg"; ArgSsr "seqdir"; ArgSsr "seqarg"]
 
-let tclseq_expr loc tac dir arg =
+let tclseq_expr ?loc tac dir arg =
   let arg1 = in_gen (rawwit wit_ssrtclarg) tac in
   let arg2 = in_gen (rawwit wit_ssrseqdir) dir in
   let arg3 = in_gen (rawwit wit_ssrseqarg) (check_seqtacarg dir arg) in
-  ssrtac_expr loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric x) [arg1; arg2; arg3])
+  ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric x) [arg1; arg2; arg3])
 
 GEXTEND Gram
   GLOBAL: tactic_expr;
   ssr_first: [
-    [ tac = ssr_first; ipats = ssrintros_ne -> tclintros_expr !@loc tac ipats
+    [ tac = ssr_first; ipats = ssrintros_ne -> tclintros_expr ~loc:!@loc tac ipats
     | "["; tacl = LIST0 tactic_expr SEP "|"; "]" -> TacFirst tacl
     ] ];
   ssr_first_else: [
@@ -3351,9 +3352,9 @@ GEXTEND Gram
     [ tac1 = tactic_expr; ";"; IDENT "first"; tac2 = ssr_first_else ->
       TacThen (tac1, tac2)
     | tac = tactic_expr; ";"; IDENT "first"; arg = ssrseqarg ->
-      tclseq_expr !@loc tac L2R arg
+      tclseq_expr ~loc:!@loc tac L2R arg
     | tac = tactic_expr; ";"; IDENT "last"; arg = ssrseqarg ->
-      tclseq_expr !@loc tac R2L arg
+      tclseq_expr ~loc:!@loc tac R2L arg
     ] ];
 END
 (* }}} *)
@@ -3378,18 +3379,18 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
    let n_binders = ref 0 in
    let ty = match ty with
    | a, (t, None) ->
-     let rec force_type = function
-     | GProd (l, x, k, s, t) -> incr n_binders; GProd (l, x, k, s, force_type t)
-     | GLetIn (l, x, v, oty, t) -> incr n_binders; GLetIn (l, x, v, oty, force_type t)
-     | ty -> mkRCast ty mkRType in
+     let rec force_type ty = CAst.(map (function
+     | GProd (x, k, s, t) -> incr n_binders; GProd (x, k, s, force_type t)
+     | GLetIn (x, v, oty, t) -> incr n_binders; GLetIn (x, v, oty, force_type t)
+     | _ -> (mkRCast ty mkRType).v)) ty in
      a, (force_type t, None)
    | _, (_, Some ty) ->
-     let rec force_type = function
-     | CProdN (l, abs, t) ->
+     let rec force_type ty = CAst.(map (function
+     | CProdN (abs, t) ->
        n_binders := !n_binders +  List.length (List.flatten (List.map pi1 abs));
-       CProdN (l, abs, force_type t)
-     | CLetIn (l, n, v, oty, t) -> incr n_binders; CLetIn (l, n, v, oty, force_type t)
-     | ty -> mkCCast dummy_loc ty (mkCType dummy_loc) in
+       CProdN (abs, force_type t)
+     | CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t)
+     | _ -> (mkCCast ty (mkCType None)).v)) ty in
      mk_term ' ' (force_type ty) in
    let strip_cast (sigma, t) =
      let rec aux t = match EConstr.kind_of_type sigma t with
@@ -3478,7 +3479,7 @@ ARGUMENT EXTEND ssrgen TYPED AS ssrdocc * cpattern PRINTED BY pr_ssrgen
 END
 
 let has_occ ((_, occ), _) = occ <> None
-let hyp_of_var sigma v =  SsrHyp (dummy_loc, EConstr.destVar sigma v)
+let hyp_of_var sigma v = SsrHyp (Loc.tag @@ EConstr.destVar sigma v)
 
 let interp_clr sigma = function
 | Some clr, (k, c) 
@@ -3509,7 +3510,7 @@ let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) =
     let p = EConstr.of_constr p in
     let gl, pty = pfe_type_of gl p in
     false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl
-  else loc_error (loc_of_cpattern t) "generalized term didn't match"
+  else loc_error ?loc:(loc_of_cpattern t) "generalized term didn't match"
 
 let genclrtac cl cs clr =
   let tclmyORELSE tac1 tac2 gl =
@@ -3665,10 +3666,10 @@ GEXTEND Gram
     | "?" -> IpatAnon
     | occ = ssrdocc; "->" -> (match occ with
       | None, occ -> IpatRw (occ, L2R)
-      | _ -> loc_error !@loc "Only occurrences are allowed here")
+      | _ -> loc_error ~loc:!@loc "Only occurrences are allowed here")
     | occ = ssrdocc; "<-" -> (match occ with
       | None, occ ->  IpatRw (occ, R2L)
-      | _ -> loc_error !@loc "Only occurrences are allowed here")
+      | _ -> loc_error ~loc:!@loc "Only occurrences are allowed here")
     | "->" -> IpatRw (allocc, L2R)
     | "<-" -> IpatRw (allocc, R2L)
     ]];
@@ -4396,10 +4397,11 @@ let interp_agen ist gl ((goclr, _), (k, gc)) (clr, rcs) =
   | Some ghyps ->
     let clr' = snd (interp_hyps ist gl ghyps) @ clr in
     if k <> ' ' then clr', rcs' else
+    let open CAst in
     match rc with
-    | GVar (loc, id) when not_section_id id -> SsrHyp (loc, id) :: clr', rcs'
-    | GRef (loc, VarRef id, _) when not_section_id id ->
-        SsrHyp (loc, id) :: clr', rcs'
+    | { loc; v = GVar id } when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs'
+    | { loc; v = GRef (VarRef id, _) } when not_section_id id ->
+        SsrHyp (Loc.tag ?loc id) :: clr', rcs'
     | _ -> clr', rcs'
 
 let interp_agens ist gl gagens =
@@ -4417,8 +4419,9 @@ let interp_agens ist gl gagens =
 
 let apply_rconstr ?ist t gl =
 (* pp(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *)
+  let open CAst in
   let n = match ist, t with
-    | None, (GVar (_, id) | GRef (_, VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id)
+    | None, { v = GVar id | GRef (VarRef id,_) } -> pf_nbargs gl (EConstr.mkVar id)
     | Some ist, _ -> interp_nbargs ist gl t
     | _ -> anomaly "apply_rconstr without ist and not RVar" in
   let mkRlemma i = mkRApp t (mkRHoles i) in
@@ -4520,8 +4523,8 @@ ARGUMENT EXTEND ssrcongrarg TYPED AS (int * ssrterm) * ssrdgens
 END
 
 let rec mkRnat n =
-  if n <= 0 then GRef (dummy_loc, glob_O, None) else
-  mkRApp (GRef (dummy_loc, glob_S, None)) [mkRnat (n - 1)]
+  if n <= 0 then CAst.make @@ GRef (glob_O, None) else
+  mkRApp (CAst.make @@ GRef (glob_S, None)) [mkRnat (n - 1)]
 
 let interp_congrarg_at ist gl n rf ty m =
   pp(lazy(str"===interp_congrarg_at==="));
@@ -4636,7 +4639,7 @@ let pr_mult (n, m) =
 let pr_ssrmult _ _ _ = pr_mult
 
 ARGUMENT EXTEND ssrmult_ne TYPED AS int * ssrmmod PRINTED BY pr_ssrmult
-  | [ natural(n) ssrmmod(m) ] -> [ check_index loc n, m ]
+  | [ natural(n) ssrmmod(m) ] -> [ check_index ~loc n, m ]
   | [ ssrmmod(m) ]            -> [ notimes, m ]
 END
 
@@ -4679,7 +4682,7 @@ let pr_rule = function
 
 let pr_ssrrule _ _ _ = pr_rule
 
-let noruleterm loc = mk_term ' ' (mkCProp loc)
+let noruleterm loc = mk_term ' ' (mkCProp (Some loc))
 
 ARGUMENT EXTEND ssrrule_ne TYPED AS ssrrwkind * ssrterm PRINTED BY pr_ssrrule
   | [ ssrsimpl_ne(s) ] -> [ RWred s, noruleterm loc ]
@@ -5404,24 +5407,24 @@ let rec format_local_binders h0 bl0 = match h0, bl0 with
     Bdef (x, oty, v) :: format_local_binders h bl
   | _ -> []
   
-let rec format_constr_expr h0 c0 = match h0, c0 with
-  | BFvar :: h, CLambdaN (_, [[_, x], _, _], c) ->
+let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
+  | BFvar :: h, { v = CLambdaN ([[_, x], _, _], c) } ->
     let bs, c' = format_constr_expr h c in
     Bvar x :: bs, c'
-  | BFdecl _:: h, CLambdaN (_, [lxs, _, t], c) ->
+  | BFdecl _:: h, { v = CLambdaN ([lxs, _, t], c) } ->
     let bs, c' = format_constr_expr h c in
     Bdecl (List.map snd lxs, t) :: bs, c'
-  | BFdef :: h, CLetIn(_, (_, x), v, oty, c) ->
+  | BFdef :: h, { v = CLetIn((_, x), v, oty, c) } ->
     let bs, c' = format_constr_expr h c in
     Bdef (x, oty, v) :: bs, c'
-  | [BFcast], CCast (_, c, CastConv t) ->
+  | [BFcast], { v = CCast (c, CastConv t) } ->
     [Bcast t], c
   | BFrec (has_str, has_cast) :: h, 
-    CFix (_, _, [_, (Some locn, CStructRec), bl, t, c]) ->
+    { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } ->
     let bs = format_local_binders h bl in
     let bstr = if has_str then [Bstruct (Name (snd locn))] else [] in
     bs @ bstr @ (if has_cast then [Bcast t] else []), c 
-  | BFrec (_, has_cast) :: h, CCoFix (_, _, [_, bl, t, c]) ->
+  | BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, bl, t, c]) } ->
     format_local_binders h bl @ (if has_cast then [Bcast t] else []), c
   | _, c ->
     [], c
@@ -5444,24 +5447,24 @@ let rec format_glob_decl h0 d0 = match h0, d0 with
      Bdef (x, None, v) :: format_glob_decl [] d
   | _, [] -> []
 
-let rec format_glob_constr h0 c0 = match h0, c0 with
-  | BFvar :: h, GLambda (_, x, _, _, c) ->
+let rec format_glob_constr h0 c0 = let open CAst in match h0, c0 with
+  | BFvar :: h, { v = GLambda (x, _, _, c) } ->
     let bs, c' = format_glob_constr h c in
     Bvar x :: bs, c'
-  | BFdecl 1 :: h,  GLambda (_, x, _, t, c) ->
+  | BFdecl 1 :: h, { v = GLambda (x, _, t, c) } ->
     let bs, c' = format_glob_constr h c in
     Bdecl ([x], t) :: bs, c'
-  | BFdecl n :: h,  GLambda (_, x, _, t, c) when n > 1 ->
+  | BFdecl n :: h, { v = GLambda (x, _, t, c) } when n > 1 ->
     begin match format_glob_constr (BFdecl (n - 1) :: h) c with
     | Bdecl (xs, _) :: bs, c' -> Bdecl (x :: xs, t) :: bs, c'
     | _ -> [Bdecl ([x], t)], c
     end
-  | BFdef :: h, GLetIn(_, x, v, oty, c) ->
+  | BFdef :: h, { v = GLetIn(x, v, oty, c) } ->
     let bs, c' = format_glob_constr h c in
     Bdef (x, oty, v) :: bs, c'
-  | [BFcast], GCast (_, c, CastConv t) ->
+  | [BFcast], { v = GCast (c, CastConv t) } ->
     [Bcast t], c
-  | BFrec (has_str, has_cast) :: h, GRec (_, f, _, bl, t, c)
+  | BFrec (has_str, has_cast) :: h, { v = GRec (f, _, bl, t, c) }
       when Array.length c = 1 ->
     let bs = format_glob_decl h bl.(0) in
     let bstr = match has_str, f with
@@ -5493,15 +5496,15 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt
 let mkFwdVal fk c = ((fk, []), mk_term ' ' c)
 let mkssrFwdVal fk c = ((fk, []), (c,None))
 
-let mkFwdCast fk loc t c = ((fk, [BFcast]), mk_term ' ' (CCast (loc, c, dC t)))
-let mkssrFwdCast fk loc t c = ((fk, [BFcast]), (c, Some t))
+let mkFwdCast fk ?loc t c = ((fk, [BFcast]), mk_term ' ' (CAst.make ?loc @@ CCast (c, dC t)))
+let mkssrFwdCast fk ?loc t c = ((fk, [BFcast]), (c, Some t))
 
 let mkFwdHint s t =
   let loc = constr_loc t in
-  mkFwdCast (FwdHint (s,false)) loc t (mkCHole loc)
+  mkFwdCast (FwdHint (s,false)) ?loc t (mkCHole ?loc)
 let mkFwdHintNoTC s t =
   let loc = constr_loc t in
-  mkFwdCast (FwdHint (s,true)) loc t (mkCHole loc)
+  mkFwdCast (FwdHint (s,true)) ?loc t (mkCHole ?loc)
 
 let pr_gen_fwd prval prc prlc fk (bs, c) =
   let prc s = str s ++ spc () ++ prval prc prlc c in
@@ -5525,7 +5528,7 @@ let pr_ssrfwd _ _ _ = pr_fwd
  
 ARGUMENT EXTEND ssrfwd TYPED AS (ssrfwdfmt * ssrterm) PRINTED BY pr_ssrfwd
   | [ ":=" lconstr(c) ] -> [ mkFwdVal FwdPose c ]
-  | [ ":" lconstr (t) ":=" lconstr(c) ] -> [ mkFwdCast FwdPose loc t c ]
+  | [ ":" lconstr (t) ":=" lconstr(c) ] -> [ mkFwdCast FwdPose ~loc t c ]
 END
 
 (** Independent parsing for binders *)
@@ -5536,13 +5539,13 @@ END
 let pr_ssrbvar prc _ _ v = prc v
 
 ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar
-| [ ident(id) ] -> [ mkCVar loc id ]
-| [ "_" ] -> [ mkCHole loc ]
+| [ ident(id) ] -> [ mkCVar ~loc id ]
+| [ "_" ] -> [ mkCHole ~loc ]
 END
 
-let bvar_lname = function
-  | CRef (Ident (loc, id), _) -> loc, Name id
-  | c -> constr_loc c, Anonymous
+let bvar_lname = let open CAst in function
+  | { v = CRef (Ident (loc, id), _) } -> Loc.tag ?loc @@ Name id
+  | { loc = loc } -> Loc.tag ?loc Anonymous
 
 let pr_ssrbinder prc _ _ (_, c) = prc c
 
@@ -5550,24 +5553,24 @@ ARGUMENT EXTEND ssrbinder TYPED AS ssrfwdfmt * constr PRINTED BY pr_ssrbinder
  | [ ssrbvar(bv) ] ->
    [ let xloc, _ as x = bvar_lname bv in
      (FwdPose, [BFvar]),
-     CLambdaN (loc,[[x],Default Explicit,mkCHole xloc],mkCHole loc) ]
+     CAst.make ~loc @@ CLambdaN ([[x],Default Explicit,mkCHole ?loc:xloc],mkCHole ~loc) ]
  | [ "(" ssrbvar(bv) ")" ] ->
    [ let xloc, _ as x = bvar_lname bv in
      (FwdPose, [BFvar]),
-     CLambdaN (loc,[[x],Default Explicit,mkCHole xloc],mkCHole loc) ]
+     CAst.make ~loc @@ CLambdaN ([[x],Default Explicit,mkCHole ?loc:xloc],mkCHole ~loc) ]
  | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
    [ let x = bvar_lname bv in
      (FwdPose, [BFdecl 1]),
-     CLambdaN (loc, [[x], Default Explicit, t], mkCHole loc) ]
+     CAst.make ~loc @@ CLambdaN ([[x], Default Explicit, t], mkCHole ~loc) ]
  | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] ->
    [ let xs = List.map bvar_lname (bv :: bvs) in
      let n = List.length xs in
      (FwdPose, [BFdecl n]),
-     CLambdaN (loc, [xs, Default Explicit, t], mkCHole loc) ]
+     CAst.make ~loc @@ CLambdaN ([xs, Default Explicit, t], mkCHole ~loc) ]
  | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] ->
-   [ (FwdPose,[BFdef]), CLetIn (loc,bvar_lname id, v, Some t, mkCHole loc) ]
+   [ (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole ~loc) ]
  | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] ->
-   [ (FwdPose,[BFdef]), CLetIn (loc,bvar_lname id, v, None, mkCHole loc) ]
+   [ (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, None, mkCHole ~loc) ]
 END
 
 GEXTEND Gram
@@ -5576,34 +5579,35 @@ GEXTEND Gram
   [  ["of" | "&"]; c = operconstr LEVEL "99" ->
      let loc = !@loc in
      (FwdPose, [BFvar]),
-     CLambdaN (loc,[[loc,Anonymous],Default Explicit,c],mkCHole loc) ]
+     CAst.make ~loc @@ CLambdaN ([[Loc.tag ~loc Anonymous],Default Explicit,c],mkCHole ~loc) ]
   ];
 END
 
-let rec binders_fmts = function
+let rec binders_fmts : (ssrfwdfmt * constr_expr) list -> _ = function
   | ((_, h), _) :: bs -> h @ binders_fmts bs
   | _ -> []
 
 let push_binders c2 bs =
-  let loc2 = constr_loc c2 in let mkloc loc1 = Loc.join_loc loc1 loc2 in
+  let loc2 = constr_loc c2 in let mkloc loc1 = Loc.merge_opt loc1 loc2 in
+  let open CAst in
   let rec loop ty c = function
-  | (_, CLambdaN (loc1, b, _)) :: bs when ty ->
-      CProdN (mkloc loc1, b, loop ty c bs)
-  | (_, CLambdaN (loc1, b, _)) :: bs ->
-      CLambdaN (mkloc loc1, b, loop ty c bs)
-  | (_, CLetIn (loc1, x, v, oty, _)) :: bs ->
-      CLetIn (mkloc loc1, x, v, oty, loop ty c bs)
+  | (_, { loc = loc1; v = CLambdaN (b, _) } ) :: bs when ty ->
+      CAst.make ?loc:(mkloc loc1) @@ CProdN (b, loop ty c bs)
+  | (_, { loc = loc1; v = CLambdaN (b, _) } ) :: bs ->
+      CAst.make ?loc:(mkloc loc1) @@ CLambdaN (b, loop ty c bs)
+  | (_, { loc = loc1; v = CLetIn (x, v, oty, _) } ) :: bs ->
+      CAst.make ?loc:(mkloc loc1) @@ CLetIn (x, v, oty, loop ty c bs)
   | [] -> c
   | _ -> anomaly "binder not a lambda nor a let in" in
   match c2 with
-  | CCast (x, ct, CastConv cty) ->
-      (CCast (x, loop false ct bs, CastConv (loop true cty bs)))
+  | { loc; v = CCast (ct, CastConv cty) } ->
+      CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs)))
   | ct -> loop false ct bs
 
-let rec fix_binders = function
-  | (_, CLambdaN (_, [xs, _, t], _)) :: bs ->
+let rec fix_binders = let open CAst in function
+  | (_, { v = CLambdaN ([xs, _, t], _) } ) :: bs ->
       CLocalAssum (xs, Default Explicit, t) :: fix_binders bs
-  | (_, CLetIn (_, x, v, oty, _)) :: bs ->
+  | (_, { v = CLetIn (x, v, oty, _) } ) :: bs ->
     CLocalDef (x, v, oty) :: fix_binders bs
   | _ -> []
 
@@ -5620,7 +5624,7 @@ END
 
 (* The plain pose form. *)
 
-let bind_fwd bs = function
+let bind_fwd (bs : (ssrfwdfmt * Constrexpr.constr_expr) list) = function
   | (fk, h), (ck, (rc, Some c)) ->
     (fk,binders_fmts bs @ h), (ck,(rc,Some (push_binders c bs)))
   | fwd -> fwd
@@ -5634,7 +5638,7 @@ END
 let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd
 
 let bvar_locid = function
-  | CRef (Ident (loc, id), _) -> loc, id
+  | { CAst.v = CRef (Ident (loc, id), _) } -> loc, id
   | _ -> CErrors.error "Missing identifier after \"(co)fix\""
 
 
@@ -5645,7 +5649,7 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd
       let c = Option.get oc in
       let has_cast, t', c' = match format_constr_expr h c with
       | [Bcast t'], c' -> true, t', c'
-      | _ -> false, mkCHole (constr_loc c), c in
+      | _ -> false, mkCHole ?loc:(constr_loc c), c in
       let lb = fix_binders bs in
       let has_struct, i =
         let rec loop = function
@@ -5655,7 +5659,7 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd
           | [] -> CErrors.error "Bad structural argument" in
         loop (names_of_local_assums lb) in
       let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in
-      let fix = CFix (loc, lid, [lid, (Some i, CStructRec), lb, t', c']) in
+      let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some i, CStructRec), lb, t', c']) in
       id, ((fk, h'), (ck, (rc, Some fix))) ]
 END
 
@@ -5671,9 +5675,9 @@ ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd
       let c = Option.get oc in
       let has_cast, t', c' = match format_constr_expr h c with
       | [Bcast t'], c' -> true, t', c'
-      | _ -> false, mkCHole (constr_loc c), c in
+      | _ -> false, mkCHole ?loc:(constr_loc c), c in
       let h' = BFrec (false, has_cast) :: binders_fmts bs in
-      let cofix = CCoFix (loc, lid, [lid, fix_binders bs, t', c']) in
+      let cofix = CAst.make ~loc @@ CCoFix (lid, [lid, fix_binders bs, t', c']) in
       id, ((fk, h'), (ck, (rc, Some cofix)))
     ]
 END
@@ -5716,9 +5720,9 @@ ARGUMENT EXTEND ssrsetfwd
 TYPED AS (ssrfwdfmt * (lcpattern * ssrterm option)) * ssrdocc
 PRINTED BY pr_ssrsetfwd
 | [ ":" lconstr(t) ":=" "{" ssrocc(occ) "}" cpattern(c) ] ->
-  [ mkssrFwdCast FwdPose loc (mk_lterm t) c, mkocc occ ]
+  [ mkssrFwdCast FwdPose ~loc (mk_lterm t) c, mkocc occ ]
 | [ ":" lconstr(t) ":=" lcpattern(c) ] ->
-  [ mkssrFwdCast FwdPose loc (mk_lterm t) c, nodocc ]
+  [ mkssrFwdCast FwdPose ~loc (mk_lterm t) c, nodocc ]
 | [ ":=" "{" ssrocc(occ) "}" cpattern(c) ] ->
   [ mkssrFwdVal FwdPose c, mkocc occ ]
 | [ ":=" lcpattern(c) ] -> [ mkssrFwdVal FwdPose c, nodocc ]
@@ -5753,26 +5757,26 @@ let pr_ssrhavefwd _ _ prt (fwd, hint) = pr_fwd fwd ++ pr_hint prt hint
 
 ARGUMENT EXTEND ssrhavefwd TYPED AS ssrfwd * ssrhint PRINTED BY pr_ssrhavefwd
 | [ ":" lconstr(t) ssrhint(hint) ] -> [ mkFwdHint ":" t, hint ]
-| [ ":" lconstr(t) ":=" lconstr(c) ] -> [ mkFwdCast FwdHave loc t c, nohint ]
+| [ ":" lconstr(t) ":=" lconstr(c) ] -> [ mkFwdCast FwdHave ~loc t c, nohint ]
 | [ ":" lconstr(t) ":=" ] -> [ mkFwdHintNoTC ":" t, nohint ]
 | [ ":=" lconstr(c) ] -> [ mkFwdVal FwdHave c, nohint ]
 END
 
 let intro_id_to_binder = List.map (function 
   | IpatId id ->
-      let xloc, _ as x = bvar_lname (mkCVar dummy_loc id) in
+      let xloc, _ as x = bvar_lname (mkCVar id) in
       (FwdPose, [BFvar]),
-        CLambdaN (dummy_loc, [[x], Default Explicit, mkCHole xloc],
-          mkCHole dummy_loc)
+        CAst.make @@ CLambdaN ([[x], Default Explicit, mkCHole ?loc:xloc],
+          mkCHole ?loc:None)
   | _ -> anomaly "non-id accepted as binder")
 
-let binder_to_intro_id = List.map (function
-  | (FwdPose, [BFvar]), CLambdaN (_,[ids,_,_],_)
-  | (FwdPose, [BFdecl _]), CLambdaN (_,[ids,_,_],_) ->
+let binder_to_intro_id = CAst.(List.map (function
+  | (FwdPose, [BFvar]), { v = CLambdaN ([ids,_,_],_) }
+  | (FwdPose, [BFdecl _]), { v = CLambdaN ([ids,_,_],_) } ->
       List.map (function (_, Name id) -> IpatId id | _ -> IpatAnon) ids
-  | (FwdPose, [BFdef]), CLetIn (_,(_,Name id),_,_,_) -> [IpatId id]
-  | (FwdPose, [BFdef]), CLetIn (_,(_,Anonymous),_,_,_) -> [IpatAnon]
-  | _ -> anomaly "ssrbinder is not a binder")
+  | (FwdPose, [BFdef]), { v = CLetIn ((_,Name id),_,_,_) } -> [IpatId id]
+  | (FwdPose, [BFdef]), { v = CLetIn ((_,Anonymous),_,_,_) } -> [IpatAnon]
+  | _ -> anomaly "ssrbinder is not a binder"))
 
 let pr_ssrhavefwdwbinders _ _ prt (tr,((hpats, (fwd, hint)))) =
   pr_hpats hpats ++ pr_fwd fwd ++ pr_hint prt hint
@@ -5880,21 +5884,22 @@ let havetac ist
   let interp gl rtc t = pf_abs_ssrterm ~resolve_typeclasses:rtc ist gl t in
   let interp_ty gl rtc t =
     let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc ist gl t in a,b,u in
+  let open CAst in
   let ct, cty, hole, loc = match t with
-    | _, (_, Some (CCast (loc, ct, CastConv cty))) ->
-      mkt ct, mkt cty, mkt (mkCHole dummy_loc), loc
+    | _, (_, Some { loc; v = CCast (ct, CastConv cty)}) ->
+      mkt ct, mkt cty, mkt (mkCHole ?loc:None), loc
     | _, (_, Some ct) ->
-      mkt ct, mkt (mkCHole dummy_loc), mkt (mkCHole dummy_loc), dummy_loc
-    | _, (GCast (loc, ct, CastConv cty), None) ->
+      mkt ct, mkt (mkCHole ?loc:None), mkt (mkCHole ?loc:None), None
+    | _, ({ loc; v = GCast (ct, CastConv cty) }, None) ->
       mkl ct, mkl cty, mkl mkRHole, loc
-    | _, (t, None) -> mkl t, mkl mkRHole, mkl mkRHole, dummy_loc in
+    | _, (t, None) -> mkl t, mkl mkRHole, mkl mkRHole, None in
   let gl, cut, sol, itac1, itac2 =
    match fk, namefst, suff with
    | FwdHave, true, true ->
      errorstrm (str"Suff have does not accept a proof term")
    | FwdHave, false, true ->
-     let cty = combineCG cty hole (mkCArrow loc) mkRArrow in
-     let _,t,uc,_ = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in
+     let cty = combineCG cty hole (mkCArrow ?loc) mkRArrow in
+     let _,t,uc,_ = interp gl false (combineCG ct cty (mkCCast ?loc) mkRCast) in
      let gl = pf_merge_uc uc gl in
      let gl, ty = pf_type_of gl t in
      let ctx, _ = decompose_prod_n 1 ty in
@@ -5911,7 +5916,7 @@ let havetac ist
        List.map (fun id -> examine_abstract (mkVar id) gl) skols in
      let gl = List.fold_right unlock_abs skols_args gl in
      let sigma, t, uc, n_evars =
-       interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in
+       interp gl false (combineCG ct cty (mkCCast ?loc) mkRCast) in
      if skols <> [] && n_evars <> 0 then
        CErrors.error ("Automatic generalization of unresolved implicit "^
                      "arguments together with abstract variables is "^
@@ -6015,7 +6020,7 @@ GEXTEND Gram
   GLOBAL: tactic_expr;
   tactic_expr: LEVEL "3"
     [ RIGHTA [ IDENT "abstract"; gens = ssrdgens ->
-               ssrtac_expr !@loc "abstract"
+               ssrtac_expr ~loc:!@loc "abstract"
                 [Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] ]];
 END
 TACTIC EXTEND ssrabstract
@@ -6070,9 +6075,10 @@ END
 
 let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
   let htac = tclTHEN (introstac ~ist pats) (hinttac ist true hint) in
+  let open CAst in
   let c = match c with
-  | (a, (b, Some (CCast (_, _, CastConv cty)))) -> a, (b, Some cty)
-  | (a, (GCast (_, _, CastConv cty), None)) -> a, (cty, None)
+  | (a, (b, Some { v = CCast (_, CastConv cty)})) -> a, (b, Some cty)
+  | (a, ({ v = GCast (_, CastConv cty) }, None)) -> a, (cty, None)
   | _ -> anomaly "suff: ssr cast hole deleted by typecheck" in
   let ctac gl =
     let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
@@ -6111,9 +6117,10 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
   let mkpats = function
   | _, Some ((x, _), _) -> fun pats -> IpatId (hoi_id x) :: pats
   | _ -> fun x -> x in
+  let open CAst in
   let ct = match ct with
-  | (a, (b, Some (CCast (_, _, CastConv cty)))) -> a, (b, Some cty)
-  | (a, (GCast (_, _, CastConv cty), None)) -> a, (cty, None)
+  | (a, (b, Some { v = CCast (_, CastConv cty)})) -> a, (b, Some cty)
+  | (a, ({ v = GCast (_, CastConv cty) }, None)) -> a, (cty, None)
   | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" in
   let cut_implies_goal = not (suff || ghave <> `NoGen) in
   let c, args, ct, gl =
@@ -6273,7 +6280,7 @@ GEXTEND Gram
           let s = coerce_reference_to_id qid in
 	  Vernacexpr.VernacDefinition
 	    ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure),
-             ((dummy_loc,s),None),(d  ))
+             ((Loc.tag s),None),(d  ))
   ]];
 END
 
@@ -6303,9 +6310,9 @@ GEXTEND Gram
   GLOBAL: hloc;
 hloc: [
   [ "in"; "("; "Type"; "of"; id = ident; ")" -> 
-    HypLocation ((dummy_loc,id), InHypTypeOnly)
+    HypLocation ((Loc.tag id), InHypTypeOnly)
   | "in"; "("; IDENT "Value"; "of"; id = ident; ")" -> 
-    HypLocation ((dummy_loc,id), InHypValueOnly)
+    HypLocation ((Loc.tag id), InHypValueOnly)
   ] ];
 END