Uniform handling of locations in the various AST.

7 files changed, 288 insertions, 297 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index bfd2ab1a11..338711e79c 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -86,19 +86,19 @@ let tac2mode = Gram.entry_create "vernac:ltac2_command"
 (** FUCK YOU API *)
 let ltac1_expr = (Obj.magic Pltac.tactic_expr : Tacexpr.raw_tactic_expr Gram.entry)
 
-let inj_wit wit loc x = CTacExt (loc, wit, x)
+let inj_wit wit loc x = Loc.tag ~loc @@ CTacExt (wit, x)
 let inj_open_constr loc c = inj_wit Tac2env.wit_open_constr loc c
 let inj_pattern loc c = inj_wit Tac2env.wit_pattern loc c
 let inj_reference loc c = inj_wit Tac2env.wit_reference loc c
 let inj_ltac1 loc e = inj_wit Tac2env.wit_ltac1 loc e
 
-let pattern_of_qualid loc id =
-  if Tac2env.is_constructor (snd id) then CPatRef (loc, RelId id, [])
+let pattern_of_qualid ?loc id =
+  if Tac2env.is_constructor (snd id) then Loc.tag ?loc @@ CPatRef (RelId id, [])
   else
     let (dp, id) = Libnames.repr_qualid (snd id) in
-    if DirPath.is_empty dp then CPatVar (Some loc, Name id)
+    if DirPath.is_empty dp then Loc.tag ?loc @@ CPatVar (Name id)
     else
-      CErrors.user_err ~loc (Pp.str "Syntax error")
+      CErrors.user_err ?loc (Pp.str "Syntax error")
 
 GEXTEND Gram
   GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn
@@ -107,53 +107,62 @@ GEXTEND Gram
     [ "1" LEFTA
       [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" ->
         if Tac2env.is_constructor (snd id) then
-          CPatRef (!@loc, RelId id, pl)
+          Loc.tag ~loc:!@loc @@ CPatRef (RelId id, pl)
         else
           CErrors.user_err ~loc:!@loc (Pp.str "Syntax error")
-      | id = Prim.qualid -> pattern_of_qualid !@loc id
-      | "["; "]" -> CPatRef (!@loc, AbsKn (Other Tac2core.Core.c_nil), [])
+      | id = Prim.qualid -> pattern_of_qualid ~loc:!@loc id
+      | "["; "]" -> Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_nil), [])
       | p1 = tac2pat; "::"; p2 = tac2pat ->
-        CPatRef (!@loc, AbsKn (Other Tac2core.Core.c_cons), [p1; p2])
+        Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_cons), [p1; p2])
       ]
     | "0"
-      [ "_" -> CPatVar (Some !@loc, Anonymous)
-      | "()" -> CPatRef (!@loc, AbsKn (Tuple 0), [])
-      | id = Prim.qualid -> pattern_of_qualid !@loc id
+      [ "_" -> Loc.tag ~loc:!@loc @@ CPatVar Anonymous
+      | "()" -> Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Tuple 0), [])
+      | id = Prim.qualid -> pattern_of_qualid ~loc:!@loc id
       | "("; pl = LIST0 tac2pat LEVEL "1" SEP ","; ")" ->
-        CPatRef (!@loc, AbsKn (Tuple (List.length pl)), pl) ]
+        Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Tuple (List.length pl)), pl) ]
     ]
   ;
   tac2expr:
     [ "6" RIGHTA
-        [ e1 = SELF; ";"; e2 = SELF -> CTacSeq (!@loc, e1, e2) ]
+        [ e1 = SELF; ";"; e2 = SELF -> Loc.tag ~loc:!@loc @@ CTacSeq (e1, e2) ]
     | "5"
-      [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "6" -> CTacFun (!@loc, it, body)
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "6" ->
+        Loc.tag ~loc:!@loc @@ CTacFun (it, body)
       | "let"; isrec = rec_flag;
           lc = LIST1 let_clause SEP "with"; "in";
-          e = tac2expr LEVEL "6" -> CTacLet (!@loc, isrec, lc, e)
+          e = tac2expr LEVEL "6" ->
+        Loc.tag ~loc:!@loc @@ CTacLet (isrec, lc, e)
       | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches; "end" ->
-         CTacCse (!@loc, e, bl)
+        Loc.tag ~loc:!@loc @@ CTacCse (e, bl)
       ]
     | "4" LEFTA [ ]
     | "::" RIGHTA
       [ e1 = tac2expr; "::"; e2 = tac2expr ->
-        CTacApp (!@loc, CTacCst (!@loc, AbsKn (Other Tac2core.Core.c_cons)), [e1; e2])
+        Loc.tag ~loc:!@loc @@ CTacApp (Loc.tag ~loc:!@loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2])
       ]
     | [ e0 = SELF; ","; el = LIST1 NEXT SEP "," ->
         let el = e0 :: el in
-        CTacApp (!@loc, CTacCst (!@loc, AbsKn (Tuple (List.length el))), el) ]
+        Loc.tag ~loc:!@loc @@ CTacApp (Loc.tag ~loc:!@loc @@ CTacCst (AbsKn (Tuple (List.length el))), el) ]
     | "1" LEFTA
-      [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" -> CTacApp (!@loc, e, el)
-      | e = SELF; ".("; qid = Prim.qualid; ")" -> CTacPrj (!@loc, e, RelId qid)
-      | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "5" -> CTacSet (!@loc, e, RelId qid, r) ]
+      [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" ->
+        Loc.tag ~loc:!@loc @@ CTacApp (e, el)
+      | e = SELF; ".("; qid = Prim.qualid; ")" ->
+        Loc.tag ~loc:!@loc @@ CTacPrj (e, RelId qid)
+      | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "5" ->
+        Loc.tag ~loc:!@loc @@ CTacSet (e, RelId qid, r) ]
     | "0"
       [ "("; a = SELF; ")" -> a
-      | "("; a = SELF; ":"; t = tac2type; ")" -> CTacCnv (!@loc, a, t)
-      | "()" -> CTacCst (!@loc, AbsKn (Tuple 0))
-      | "("; ")" -> CTacCst (!@loc, AbsKn (Tuple 0))
+      | "("; a = SELF; ":"; t = tac2type; ")" ->
+        Loc.tag ~loc:!@loc @@ CTacCnv (a, t)
+      | "()" ->
+        Loc.tag ~loc:!@loc @@ CTacCst (AbsKn (Tuple 0))
+      | "("; ")" ->
+        Loc.tag ~loc:!@loc @@ CTacCst (AbsKn (Tuple 0))
       | "["; a = LIST0 tac2expr LEVEL "5" SEP ";"; "]" ->
         Tac2quote.of_list ~loc:!@loc (fun x -> x) a
-      | "{"; a = tac2rec_fieldexprs; "}" -> CTacRec (!@loc, a)
+      | "{"; a = tac2rec_fieldexprs; "}" ->
+        Loc.tag ~loc:!@loc @@ CTacRec a
       | a = tactic_atom -> a ]
     ]
   ;
@@ -178,10 +187,13 @@ GEXTEND Gram
     [ [ "'"; id = Prim.ident -> id ] ]
   ;
   tactic_atom:
-    [ [ n = Prim.integer -> CTacAtm (Loc.tag ~loc:!@loc (AtmInt n))
-      | s = Prim.string -> CTacAtm (Loc.tag ~loc:!@loc (AtmStr s))
+    [ [ n = Prim.integer -> Loc.tag ~loc:!@loc @@ CTacAtm (AtmInt n)
+      | s = Prim.string -> Loc.tag ~loc:!@loc @@ CTacAtm (AtmStr s)
       | id = Prim.qualid ->
-        if Tac2env.is_constructor (snd id) then CTacCst (!@loc, RelId id) else CTacRef (RelId id)
+        if Tac2env.is_constructor (snd id) then
+          Loc.tag ~loc:!@loc @@ CTacCst (RelId id)
+        else
+          Loc.tag ~loc:!@loc @@ CTacRef (RelId id)
       | "@"; id = Prim.ident -> Tac2quote.of_ident (Loc.tag ~loc:!@loc id)
       | "&"; id = lident -> Tac2quote.of_hyp ~loc:!@loc id
       | "'"; c = Constr.constr -> inj_open_constr !@loc c
@@ -196,35 +208,38 @@ GEXTEND Gram
   let_clause:
     [ [ binder = let_binder; ":="; te = tac2expr ->
         let (pat, fn) = binder in
-        let te = match fn with None -> te | Some args -> CTacFun (!@loc, args, te) in
+        let te = match fn with
+        | None -> te
+        | Some args -> Loc.tag ~loc:!@loc @@ CTacFun (args, te)
+        in
         (pat, None, te)
     ] ]
   ;
   let_binder:
     [ [ pats = LIST1 input_fun ->
         match pats with
-        | [CPatVar _ as pat, None] -> (pat, None)
-        | (CPatVar (_, Name id) as pat, None) :: args -> (pat, Some args)
+        | [(_, CPatVar _) as pat, None] -> (pat, None)
+        | ((_, CPatVar (Name id)) as pat, None) :: args -> (pat, Some args)
         | [pat, None] -> (pat, None)
         | _ -> CErrors.user_err ~loc:!@loc (str "Invalid pattern")
     ] ]
   ;
   tac2type:
     [ "5" RIGHTA
-      [ t1 = tac2type; "->"; t2 = tac2type -> CTypArrow (!@loc, t1, t2) ]
+      [ t1 = tac2type; "->"; t2 = tac2type -> Loc.tag ~loc:!@loc @@ CTypArrow (t1, t2) ]
     | "2"
       [ t = tac2type; "*"; tl = LIST1 tac2type LEVEL "1" SEP "*" ->
         let tl = t :: tl in
-        CTypRef (!@loc, AbsKn (Tuple (List.length tl)), tl) ]
+        Loc.tag ~loc:!@loc @@ CTypRef (AbsKn (Tuple (List.length tl)), tl) ]
     | "1" LEFTA
-      [ t = SELF; qid = Prim.qualid -> CTypRef (!@loc, RelId qid, [t]) ]
+      [ t = SELF; qid = Prim.qualid -> Loc.tag ~loc:!@loc @@ CTypRef (RelId qid, [t]) ]
     | "0"
       [ "("; t = tac2type LEVEL "5"; ")"  -> t
-      | id = typ_param -> CTypVar (Loc.tag ~loc:!@loc (Name id))
-      | "_" -> CTypVar (Loc.tag ~loc:!@loc Anonymous)
-      | qid = Prim.qualid -> CTypRef (!@loc, RelId qid, [])
+      | id = typ_param -> Loc.tag ~loc:!@loc @@ CTypVar (Name id)
+      | "_" -> Loc.tag ~loc:!@loc @@ CTypVar Anonymous
+      | qid = Prim.qualid -> Loc.tag ~loc:!@loc @@ CTypRef (RelId qid, [])
       | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid ->
-        CTypRef (!@loc, RelId qid, p) ]
+        Loc.tag ~loc:!@loc @@ CTypRef (RelId qid, p) ]
     ];
   locident:
     [ [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ]
@@ -239,7 +254,7 @@ GEXTEND Gram
   ;
   tac2def_body:
     [ [ name = binder; it = LIST0 input_fun; ":="; e = tac2expr ->
-        let e = if List.is_empty it then e else CTacFun (!@loc, it, e) in
+        let e = if List.is_empty it then e else Loc.tag ~loc:!@loc @@ CTacFun (it, e) in
         (name, e)
     ] ]
   ;
diff --git a/src/tac2core.ml b/src/tac2core.ml
index e1aa6eb48c..db8f989768 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -938,20 +938,18 @@ let add_scope s f =
 
 let scope_fail () = CErrors.user_err (str "Invalid parsing token")
 
-let dummy_loc = Loc.make_loc (-1, -1)
-
-let q_unit = CTacCst (dummy_loc, AbsKn (Tuple 0))
+let q_unit = Loc.tag @@ CTacCst (AbsKn (Tuple 0))
 
 let rthunk e =
   let loc = Tac2intern.loc_of_tacexpr e in
-  let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn (Other Core.t_unit), []))] in
-  CTacFun (loc, var, e)
+  let var = [Loc.tag ?loc @@ CPatVar Anonymous, Some (Loc.tag ?loc @@ CTypRef (AbsKn (Other Core.t_unit), []))] in
+  Loc.tag ?loc @@ CTacFun (var, e)
 
 let add_generic_scope s entry arg =
   let parse = function
   | [] ->
     let scope = Extend.Aentry entry in
-    let act x = CTacExt (dummy_loc, arg, x) in
+    let act x = Loc.tag @@ CTacExt (arg, x) in
     Tac2entries.ScopeRule (scope, act)
   | _ -> scope_fail ()
   in
@@ -1007,9 +1005,9 @@ let () = add_scope "opt" begin function
   let scope = Extend.Aopt scope in
   let act opt = match opt with
   | None ->
-    CTacCst (dummy_loc, AbsKn (Other Core.c_none))
+    Loc.tag @@ CTacCst (AbsKn (Other Core.c_none))
   | Some x ->
-    CTacApp (dummy_loc, CTacCst (dummy_loc, AbsKn (Other Core.c_some)), [act x])
+    Loc.tag @@ CTacApp (Loc.tag @@ CTacCst (AbsKn (Other Core.c_some)), [act x])
   in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index a503a0ab4c..9c5d9a659b 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -263,8 +263,6 @@ let inTypExt : typext -> obj =
 
 (** Toplevel entries *)
 
-let dummy_loc = Loc.make_loc (-1, -1)
-
 let fresh_var avoid x =
   let bad id =
     Id.Set.mem id avoid ||
@@ -275,8 +273,8 @@ let fresh_var avoid x =
 (** Mangle recursive tactics *)
 let inline_rec_tactic tactics =
   let avoid = List.fold_left (fun accu ((_, id), _) -> Id.Set.add id accu) Id.Set.empty tactics in
-  let map (id, e) = match e with
-  | CTacFun (loc, pat, _) -> (id, pat, e)
+  let map (id, e) = match snd e with
+  | CTacFun (pat, _) -> (id, pat, e)
   | _ ->
     let loc, _ = id in
     user_err ?loc (str "Recursive tactic definitions must be functions")
@@ -286,24 +284,24 @@ let inline_rec_tactic tactics =
     let fold_var (avoid, ans) (pat, _) =
       let id = fresh_var avoid "x" in
       let loc = loc_of_patexpr pat in
-      (Id.Set.add id avoid, Loc.tag ~loc id :: ans)
+      (Id.Set.add id avoid, Loc.tag ?loc id :: ans)
     in
     (** Fresh variables to abstract over the function patterns *)
     let _, vars = List.fold_left fold_var (avoid, []) pat in
-    let map_body ((loc, id), _, e) = CPatVar (loc, Name id), None, e in
+    let map_body ((loc, id), _, e) = (Loc.tag ?loc @@ CPatVar (Name id)), None, e in
     let bnd = List.map map_body tactics in
     let pat_of_id (loc, id) =
-      (CPatVar (loc, Name id), None)
+      ((Loc.tag ?loc @@ CPatVar (Name id)), None)
     in
     let var_of_id (loc, id) =
       let qid = (loc, qualid_of_ident id) in
-      CTacRef (RelId qid)
+      Loc.tag ?loc @@ CTacRef (RelId qid)
     in
     let loc0 = loc_of_tacexpr e in
     let vpat = List.map pat_of_id vars in
     let varg = List.map var_of_id vars in
-    let e = CTacLet (loc0, true, bnd, CTacApp (loc0, var_of_id id, varg)) in
-    (id, CTacFun (loc0, vpat, e))
+    let e = Loc.tag ?loc:loc0 @@ CTacLet (true, bnd, Loc.tag ?loc:loc0 @@ CTacApp (var_of_id id, varg)) in
+    (id, Loc.tag ?loc:loc0 @@ CTacFun (vpat, e))
   in
   List.map map tactics
 
@@ -459,9 +457,8 @@ let register_open ?(local = false) (loc, qid) (params, def) =
     user_err ?loc (str "Type " ++ pr_qualid qid ++ str " is not an open type")
   in
   let () =
-    let loc = Option.default dummy_loc loc in
     if not (Int.equal (List.length params) tparams) then
-      Tac2intern.error_nparams_mismatch loc (List.length params) tparams
+      Tac2intern.error_nparams_mismatch ?loc (List.length params) tparams
   in
   match def with
   | CTydOpn -> ()
@@ -524,9 +521,9 @@ module ParseToken =
 struct
 
 let loc_of_token = function
-| SexprStr (loc, _) -> Option.default dummy_loc loc
-| SexprInt (loc, _) -> Option.default dummy_loc loc
-| SexprRec (loc, _, _) -> loc
+| SexprStr (loc, _) -> loc
+| SexprInt (loc, _) -> loc
+| SexprRec (loc, _, _) -> Some loc
 
 let parse_scope = function
 | SexprRec (_, (loc, Some id), toks) ->
@@ -535,11 +532,11 @@ let parse_scope = function
   else
     CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Nameops.pr_id id)
 | SexprStr (_, str) ->
-  let v_unit = CTacCst (dummy_loc, AbsKn (Tuple 0)) in
+  let v_unit = Loc.tag @@ CTacCst (AbsKn (Tuple 0)) in
   ScopeRule (Extend.Atoken (Tok.IDENT str), (fun _ -> v_unit))
 | tok ->
   let loc = loc_of_token tok in
-  CErrors.user_err ~loc (str "Invalid parsing token")
+  CErrors.user_err ?loc (str "Invalid parsing token")
 
 let parse_token = function
 | SexprStr (_, s) -> TacTerm s
@@ -549,7 +546,7 @@ let parse_token = function
   TacNonTerm (na, scope)
 | tok ->
   let loc = loc_of_token tok in
-  CErrors.user_err ~loc (str "Invalid parsing token")
+  CErrors.user_err ?loc (str "Invalid parsing token")
 
 end
 
@@ -586,10 +583,10 @@ let perform_notation syn st =
   let mk loc args =
     let map (na, e) =
       let loc = loc_of_tacexpr e in
-      (CPatVar (Loc.tag ~loc na), None, e)
+      ((Loc.tag ?loc @@ CPatVar na), None, e)
     in
     let bnd = List.map map args in
-    CTacLet (loc, false, bnd, syn.synext_exp)
+    Loc.tag ~loc @@ CTacLet (false, bnd, syn.synext_exp)
   in
   let rule = Extend.Rule (rule, act mk) in
   let lev = match syn.synext_lev with
@@ -793,7 +790,7 @@ let solve default tac =
 let call ~default e =
   let loc = loc_of_tacexpr e in
   let (e, t) = intern e in
-  let () = check_unit ~loc t in
+  let () = check_unit ?loc t in
   let tac = Tac2interp.interp Id.Map.empty e in
   solve default (Proofview.tclIGNORE tac)
 
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index ccff8e7756..1045063cd2 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -44,10 +44,12 @@ type 'a or_tuple =
 
 (** {5 Type syntax} *)
 
-type raw_typexpr =
-| CTypVar of Name.t located
-| CTypArrow of Loc.t * raw_typexpr * raw_typexpr
-| CTypRef of Loc.t * type_constant or_tuple or_relid * raw_typexpr list
+type raw_typexpr_r =
+| CTypVar of Name.t
+| CTypArrow of raw_typexpr * raw_typexpr
+| CTypRef of type_constant or_tuple or_relid * raw_typexpr list
+
+and raw_typexpr = raw_typexpr_r located
 
 type raw_typedef =
 | CTydDef of raw_typexpr option
@@ -87,24 +89,28 @@ type atom =
 | AtmStr of string
 
 (** Tactic expressions *)
-type raw_patexpr =
-| CPatVar of Name.t located
-| CPatRef of Loc.t * ltac_constructor or_tuple or_relid * raw_patexpr list
+type raw_patexpr_r =
+| CPatVar of Name.t
+| CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
+
+and raw_patexpr = raw_patexpr_r located
 
-type raw_tacexpr =
-| CTacAtm of atom located
+type raw_tacexpr_r =
+| CTacAtm of atom
 | CTacRef of tacref or_relid
-| CTacCst of Loc.t * ltac_constructor or_tuple or_relid
-| CTacFun of Loc.t * (raw_patexpr * raw_typexpr option) list * raw_tacexpr
-| CTacApp of Loc.t * raw_tacexpr * raw_tacexpr list
-| CTacLet of Loc.t * rec_flag * (raw_patexpr * raw_typexpr option * raw_tacexpr) list * raw_tacexpr
-| CTacCnv of Loc.t * raw_tacexpr * raw_typexpr
-| CTacSeq of Loc.t * raw_tacexpr * raw_tacexpr
-| CTacCse of Loc.t * raw_tacexpr * raw_taccase list
-| CTacRec of Loc.t * raw_recexpr
-| CTacPrj of Loc.t * raw_tacexpr * ltac_projection or_relid
-| CTacSet of Loc.t * raw_tacexpr * ltac_projection or_relid * raw_tacexpr
-| CTacExt : Loc.t * ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr
+| CTacCst of ltac_constructor or_tuple or_relid
+| CTacFun of (raw_patexpr * raw_typexpr option) list * raw_tacexpr
+| CTacApp of raw_tacexpr * raw_tacexpr list
+| CTacLet of rec_flag * (raw_patexpr * raw_typexpr option * raw_tacexpr) list * raw_tacexpr
+| CTacCnv of raw_tacexpr * raw_typexpr
+| CTacSeq of raw_tacexpr * raw_tacexpr
+| CTacCse of raw_tacexpr * raw_taccase list
+| CTacRec of raw_recexpr
+| CTacPrj of raw_tacexpr * ltac_projection or_relid
+| CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
+| CTacExt : ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr_r
+
+and raw_tacexpr = raw_tacexpr_r located
 
 and raw_taccase = raw_patexpr * raw_tacexpr
 
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 2b234d7aec..c1fd281808 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -187,36 +187,18 @@ let push_name id t env = match id with
 | Anonymous -> env
 | Name id -> { env with env_var = Id.Map.add id t env.env_var }
 
-let dummy_loc = Loc.make_loc (-1, -1)
-
-let loc_of_tacexpr = function
-| CTacAtm (loc, _) -> Option.default dummy_loc loc
-| CTacRef (RelId (loc, _)) -> Option.default dummy_loc loc
-| CTacRef (AbsKn _) -> dummy_loc
-| CTacCst (loc, _) -> loc
-| CTacFun (loc, _, _) -> loc
-| CTacApp (loc, _, _) -> loc
-| CTacLet (loc, _, _, _) -> loc
-| CTacCnv (loc, _, _) -> loc
-| CTacSeq (loc, _, _) -> loc
-| CTacCse (loc, _, _) -> loc
-| CTacRec (loc, _) -> loc
-| CTacPrj (loc, _, _) -> loc
-| CTacSet (loc, _, _, _) -> loc
-| CTacExt (loc, _, _) -> loc
-
-let loc_of_patexpr = function
-| CPatVar (loc, _) -> Option.default dummy_loc loc
-| CPatRef (loc, _, _) -> loc
-
-let error_nargs_mismatch loc kn nargs nfound =
+let loc_of_tacexpr (loc, _) : Loc.t option = loc
+
+let loc_of_patexpr (loc, _) : Loc.t option = loc
+
+let error_nargs_mismatch ?loc kn nargs nfound =
   let cstr = Tac2env.shortest_qualid_of_constructor kn in
-  user_err ~loc (str "Constructor " ++ pr_qualid cstr ++ str " expects " ++
+  user_err ?loc (str "Constructor " ++ pr_qualid cstr ++ str " expects " ++
     int nargs ++ str " arguments, but is applied to " ++ int nfound ++
     str " arguments")
 
-let error_nparams_mismatch loc nargs nfound =
-  user_err ~loc (str "Type expects " ++ int nargs ++
+let error_nparams_mismatch ?loc nargs nfound =
+  user_err ?loc (str "Type expects " ++ int nargs ++
     str " arguments, but is applied to " ++ int nfound ++
     str " arguments")
 
@@ -226,10 +208,10 @@ let rec subst_type subst (t : 'a glb_typexpr) = match t with
 | GTypRef (qid, args) ->
   GTypRef (qid, List.map (fun t -> subst_type subst t) args)
 
-let rec intern_type env (t : raw_typexpr) : UF.elt glb_typexpr = match t with
-| CTypVar (loc, Name id) -> GTypVar (get_alias (Loc.tag ?loc id) env)
-| CTypVar (_, Anonymous) -> GTypVar (fresh_id env)
-| CTypRef (loc, rel, args) ->
+let rec intern_type env ((loc, t) : raw_typexpr) : UF.elt glb_typexpr = match t with
+| CTypVar (Name id) -> GTypVar (get_alias (Loc.tag ?loc id) env)
+| CTypVar Anonymous -> GTypVar (fresh_id env)
+| CTypRef (rel, args) ->
   let (kn, nparams) = match rel with
   | RelId (loc, qid) ->
     let (dp, id) = repr_qualid qid in
@@ -255,7 +237,7 @@ let rec intern_type env (t : raw_typexpr) : UF.elt glb_typexpr = match t with
     if not (Int.equal nparams nargs) then
       let loc, qid = match rel with
       | RelId lid -> lid
-      | AbsKn (Other kn) -> Some loc, shortest_qualid_of_type kn
+      | AbsKn (Other kn) -> loc, shortest_qualid_of_type kn
       | AbsKn (Tuple _) -> assert false
       in
       user_err ?loc (strbrk "The type constructor " ++ pr_qualid qid ++
@@ -263,7 +245,7 @@ let rec intern_type env (t : raw_typexpr) : UF.elt glb_typexpr = match t with
         applied to " ++ int nargs ++ strbrk "argument(s)")
   in
   GTypRef (kn, List.map (fun t -> intern_type env t) args)
-| CTypArrow (loc, t1, t2) -> GTypArrow (intern_type env t1, intern_type env t2)
+| CTypArrow (t1, t2) -> GTypArrow (intern_type env t1, intern_type env t2)
 
 let fresh_type_scheme env (t : type_scheme) : UF.elt glb_typexpr =
   let (n, t) = t in
@@ -387,7 +369,7 @@ let unify_arrow ?loc env ft args =
   let rec iter ft args is_fun = match kind env ft, args with
   | t, [] -> t
   | GTypArrow (t1, ft), (loc, t2) :: args ->
-    let () = unify ~loc env t2 t1 in
+    let () = unify ?loc env t2 t1 in
     iter ft args true
   | GTypVar id, (_, t) :: args ->
     let ft = GTypVar (fresh_id env) in
@@ -492,19 +474,19 @@ let check_elt_unit loc env t =
   | GTypRef (Tuple 0, []) -> true
   | GTypRef _ -> false
   in
-  if not maybe_unit then warn_not_unit ~loc ()
+  if not maybe_unit then warn_not_unit ?loc ()
 
 let check_elt_empty loc env t = match kind env t with
 | GTypVar _ ->
-  user_err ~loc (str "Cannot infer an empty type for this expression")
+  user_err ?loc (str "Cannot infer an empty type for this expression")
 | GTypArrow _ | GTypRef (Tuple _, _) ->
-  user_err ~loc (str "Type " ++ pr_glbtype env t ++ str " is not an empty type")
+  user_err ?loc (str "Type " ++ pr_glbtype env t ++ str " is not an empty type")
 | GTypRef (Other kn, _) ->
   let def = Tac2env.interp_type kn in
   match def with
   | _, GTydAlg { galg_constructors = [] } -> kn
   | _ ->
-    user_err ~loc (str "Type " ++ pr_glbtype env t ++ str " is not an empty type")
+    user_err ?loc (str "Type " ++ pr_glbtype env t ++ str " is not an empty type")
 
 let check_unit ?loc t =
   let env = empty_env () in
@@ -520,7 +502,7 @@ let check_unit ?loc t =
 
 let check_redundant_clause = function
 | [] -> ()
-| (p, _) :: _ -> warn_redundant_clause ~loc:(loc_of_patexpr p) ()
+| (p, _) :: _ -> warn_redundant_clause ?loc:(loc_of_patexpr p) ()
 
 let get_variable0 mem var = match var with
 | RelId (loc, qid) ->
@@ -576,9 +558,9 @@ type glb_patexpr =
 | GPatVar of Name.t
 | GPatRef of ltac_constructor or_tuple * glb_patexpr list
 
-let rec intern_patexpr env = function
-| CPatVar (_, na) -> GPatVar na
-| CPatRef (_, qid, pl) ->
+let rec intern_patexpr env (_, pat) = match pat with
+| CPatVar na -> GPatVar na
+| CPatRef (qid, pl) ->
   let kn = get_constructor env qid in
   GPatRef (kn, List.map (fun p -> intern_patexpr env p) pl)
 
@@ -619,27 +601,27 @@ let add_name accu = function
 | Name id -> Id.Set.add id accu
 | Anonymous -> accu
 
-let rec ids_of_pattern accu = function
-| CPatVar (_, Anonymous) -> accu
-| CPatVar (_, Name id) -> Id.Set.add id accu
-| CPatRef (_, _, pl) ->
+let rec ids_of_pattern accu (_, pat) = match pat with
+| CPatVar Anonymous -> accu
+| CPatVar (Name id) -> Id.Set.add id accu
+| CPatRef (_, pl) ->
   List.fold_left ids_of_pattern accu pl
 
 let loc_of_relid = function
-| RelId (loc, _) -> Option.default dummy_loc loc
-| AbsKn _ -> dummy_loc
+| RelId (loc, _) -> loc
+| AbsKn _ -> None
 
 (** Expand pattern: [p => t] becomes [x => match x with p => t end] *)
 let expand_pattern avoid bnd =
   let fold (avoid, bnd) (pat, t) =
-    let na, expand = match pat with
-    | CPatVar (_, na) ->
+    let na, expand = match snd pat with
+    | CPatVar na ->
       (** Don't expand variable patterns *)
       na, None
     | _ ->
       let loc = loc_of_patexpr pat in
       let id = fresh_var avoid in
-      let qid = RelId (Loc.tag ~loc (qualid_of_ident id)) in
+      let qid = RelId (Loc.tag ?loc (qualid_of_ident id)) in
       Name id, Some qid
     in
     let avoid = ids_of_pattern avoid pat in
@@ -649,7 +631,9 @@ let expand_pattern avoid bnd =
   let (_, bnd) = List.fold_left fold (avoid, []) bnd in
   let fold e (na, pat, expand) = match expand with
   | None -> e
-  | Some qid -> CTacCse (loc_of_relid qid, CTacRef qid, [pat, e])
+  | Some qid ->
+    let loc = loc_of_relid qid in
+    Loc.tag ?loc @@ CTacCse (Loc.tag ?loc @@ CTacRef qid, [pat, e])
   in
   let expand e = List.fold_left fold e bnd in
   let nas = List.rev_map (fun (na, _, _) -> na) bnd in
@@ -659,8 +643,8 @@ let is_alias env qid = match get_variable env qid with
 | ArgArg (TacAlias _) -> true
 | ArgVar _ | (ArgArg (TacConstant _)) -> false
 
-let rec intern_rec env = function
-| CTacAtm (_, atm) -> intern_atm env atm
+let rec intern_rec env (loc, e) = match e with
+| CTacAtm atm -> intern_atm env atm
 | CTacRef qid ->
   begin match get_variable env qid with
   | ArgVar (_, id) ->
@@ -673,10 +657,10 @@ let rec intern_rec env = function
     let e = Tac2env.interp_alias kn in
     intern_rec env e
   end
-| CTacCst (loc, qid) ->
+| CTacCst qid ->
   let kn = get_constructor env qid in
   intern_constructor env loc kn []
-| CTacFun (loc, bnd, e) ->
+| CTacFun (bnd, e) ->
   let map (_, t) = match t with
   | None -> GTypVar (fresh_id env)
   | Some t -> intern_type env t
@@ -687,10 +671,10 @@ let rec intern_rec env = function
   let (e, t) = intern_rec env (exp e) in
   let t = List.fold_right (fun t accu -> GTypArrow (t, accu)) tl t in
   (GTacFun (nas, e), t)
-| CTacApp (loc, CTacCst (_, qid), args) ->
+| CTacApp ((loc, CTacCst qid), args) ->
   let kn = get_constructor env qid in
   intern_constructor env loc kn args
-| CTacApp (loc, CTacRef qid, args) when is_alias env qid ->
+| CTacApp ((_, CTacRef qid), args) when is_alias env qid ->
   let kn = match get_variable env qid with
   | ArgArg (TacAlias kn) -> kn
   | ArgVar _ | (ArgArg (TacConstant _)) -> assert false
@@ -699,12 +683,12 @@ let rec intern_rec env = function
   let map arg =
     (** Thunk alias arguments *)
     let loc = loc_of_tacexpr arg in
-    let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn (Tuple 0), []))] in
-    CTacFun (loc, var, arg)
+    let var = [Loc.tag ?loc @@ CPatVar Anonymous, Some (Loc.tag ?loc @@ CTypRef (AbsKn (Tuple 0), []))] in
+    Loc.tag ?loc @@ CTacFun (var, arg)
   in
   let args = List.map map args in
-  intern_rec env (CTacApp (loc, e, args))
-| CTacApp (loc, f, args) ->
+  intern_rec env (Loc.tag ?loc @@ CTacApp (e, args))
+| CTacApp (f, args) ->
   let loc = loc_of_tacexpr f in
   let (f, ft) = intern_rec env f in
   let fold arg (args, t) =
@@ -713,9 +697,9 @@ let rec intern_rec env = function
     (arg :: args, (loc, argt) :: t)
   in
   let (args, t) = List.fold_right fold args ([], []) in
-  let ret = unify_arrow ~loc env ft t in
+  let ret = unify_arrow ?loc env ft t in
   (GTacApp (f, args), ret)
-| CTacLet (loc, is_rec, el, e) ->
+| CTacLet (is_rec, el, e) ->
   let fold accu (pat, _, e) =
     let ids = ids_of_pattern Id.Set.empty pat in
     let common = Id.Set.inter ids accu in
@@ -723,39 +707,39 @@ let rec intern_rec env = function
     else
       let id = Id.Set.choose common in
       let loc = loc_of_patexpr pat in
-      user_err ~loc (str "Variable " ++ Id.print id ++ str " is bound several \
+      user_err ?loc (str "Variable " ++ Id.print id ++ str " is bound several \
         times in this matching")
   in
   let ids = List.fold_left fold Id.Set.empty el in
   if is_rec then intern_let_rec env loc ids el e
   else intern_let env loc ids el e
-| CTacCnv (loc, e, tc) ->
+| CTacCnv (e, tc) ->
   let (e, t) = intern_rec env e in
   let tc = intern_type env tc in
-  let () = unify ~loc env t tc in
+  let () = unify ?loc env t tc in
   (e, tc)
-| CTacSeq (loc, e1, e2) ->
+| CTacSeq (e1, e2) ->
   let loc1 = loc_of_tacexpr e1 in
   let (e1, t1) = intern_rec env e1 in
   let (e2, t2) = intern_rec env e2 in
   let () = check_elt_unit loc1 env t1 in
   (GTacLet (false, [Anonymous, e1], e2), t2)
-| CTacCse (loc, e, pl) ->
+| CTacCse (e, pl) ->
   intern_case env loc e pl
-| CTacRec (loc, fs) ->
+| CTacRec fs ->
   intern_record env loc fs
-| CTacPrj (loc, e, proj) ->
+| CTacPrj (e, proj) ->
   let pinfo = get_projection proj in
   let loc = loc_of_tacexpr e in
   let (e, t) = intern_rec env e in
   let subst = Array.init pinfo.pdata_prms (fun _ -> fresh_id env) in
   let params = Array.map_to_list (fun i -> GTypVar i) subst in
   let exp = GTypRef (Other pinfo.pdata_type, params) in
-  let () = unify ~loc env t exp in
+  let () = unify ?loc env t exp in
   let substf i = GTypVar subst.(i) in
   let ret = subst_type substf pinfo.pdata_ptyp in
   (GTacPrj (pinfo.pdata_type, e, pinfo.pdata_indx), ret)
-| CTacSet (loc, e, proj, r) ->
+| CTacSet (e, proj, r) ->
   let pinfo = get_projection proj in
   let () =
     if not pinfo.pdata_mutb then
@@ -773,7 +757,7 @@ let rec intern_rec env = function
   let ret = subst_type substf pinfo.pdata_ptyp in
   let r = intern_rec_with_constraint env r ret in
   (GTacSet (pinfo.pdata_type, e, pinfo.pdata_indx, r), GTypRef (Tuple 0, []))
-| CTacExt (loc, tag, arg) ->
+| CTacExt (tag, arg) ->
   let open Genintern in
   let self ist e =
     let env = match Store.get ist.extra ltac2_env with
@@ -798,7 +782,7 @@ let rec intern_rec env = function
 and intern_rec_with_constraint env e exp =
   let loc = loc_of_tacexpr e in
   let (e, t) = intern_rec env e in
-  let () = unify ~loc env t exp in
+  let () = unify ?loc env t exp in
   e
 
 and intern_let env loc ids el e =
@@ -827,11 +811,11 @@ and intern_let env loc ids el e =
 
 and intern_let_rec env loc ids el e =
   let map env (pat, t, e) =
-    let loc, na = match pat with
+    let (loc, pat) = pat in
+    let na = match pat with
     | CPatVar na -> na
     | CPatRef _ ->
-      let loc = loc_of_patexpr pat in
-      user_err ~loc (str "This kind of pattern is forbidden in let-rec bindings")
+      user_err ?loc (str "This kind of pattern is forbidden in let-rec bindings")
     in
     let id = fresh_id env in
     let env = push_name na (monomorphic (GTypVar id)) env in
@@ -843,7 +827,7 @@ and intern_let_rec env loc ids el e =
     let (e, t) = intern_rec env e in
     let () =
       if not (is_rec_rhs e) then
-        user_err ~loc:loc_e (str "This kind of expression is not allowed as \
+        user_err ?loc:loc_e (str "This kind of expression is not allowed as \
           right-hand side of a recursive binding")
     in
     let () = unify ?loc env t (GTypVar id) in
@@ -881,7 +865,7 @@ and intern_case env loc e pl =
     (GTacCse (e', Other kn, [||], [||]), GTypVar r)
   | PKind_variant kn ->
     let subst, tc = fresh_reftype env kn in
-    let () = unify ~loc:(loc_of_tacexpr e) env t tc in
+    let () = unify ?loc:(loc_of_tacexpr e) env t tc in
     let (nconst, nnonconst, arities) = match kn with
     | Tuple 0 -> 1, 0, [0]
     | Tuple n -> 0, 1, [n]
@@ -897,9 +881,11 @@ and intern_case env loc e pl =
     let rec intern_branch = function
     | [] -> ()
     | (pat, br) :: rem ->
-      let tbr = match pat with
-      | CPatVar (loc, Name _) -> todo ?loc ()
-      | CPatVar (_, Anonymous) ->
+      let tbr = match snd pat with
+      | CPatVar (Name _) ->
+        let loc = loc_of_patexpr pat in
+        todo ?loc ()
+      | CPatVar Anonymous ->
         let () = check_redundant_clause rem in
         let (br', brT) = intern_rec env br in
         (** Fill all remaining branches *)
@@ -919,7 +905,8 @@ and intern_case env loc e pl =
         in
         let _ = List.fold_left fill (0, 0) arities in
         brT
-      | CPatRef (loc, qid, args) ->
+      | CPatRef (qid, args) ->
+        let loc = loc_of_patexpr pat in
         let knc = get_constructor env qid in
         let kn', index, arity = match knc with
         | Tuple n -> Tuple n, 0, List.init n (fun i -> GTypVar i)
@@ -930,11 +917,11 @@ and intern_case env loc e pl =
         in
         let () =
           if not (eq_or_tuple KerName.equal kn kn') then
-            invalid_pattern ~loc kn kn'
+            invalid_pattern ?loc kn kn'
         in
-        let get_id = function
-        | CPatVar (_, na) -> na
-        | p -> todo ~loc:(loc_of_patexpr p) ()
+        let get_id pat = match pat with
+        | _, CPatVar na -> na
+        | loc, _ -> todo ?loc ()
         in
         let ids = List.map get_id args in
         let nids = List.length ids in
@@ -942,7 +929,7 @@ and intern_case env loc e pl =
         let () = match knc with
         | Tuple n -> assert (n == nids)
         | Other knc ->
-          if not (Int.equal nids nargs) then error_nargs_mismatch loc knc nargs nids
+          if not (Int.equal nids nargs) then error_nargs_mismatch ?loc knc nargs nids
         in
         let fold env id tpe =
           (** Instantiate all arguments *)
@@ -955,15 +942,15 @@ and intern_case env loc e pl =
         let () =
           if List.is_empty args then
             if Option.is_empty const.(index) then const.(index) <- Some br'
-            else warn_redundant_clause ~loc ()
+            else warn_redundant_clause ?loc ()
           else
             let ids = Array.of_list ids in
             if Option.is_empty nonconst.(index) then nonconst.(index) <- Some (ids, br')
-            else warn_redundant_clause ~loc ()
+            else warn_redundant_clause ?loc ()
         in
         brT
       in
-      let () = unify ~loc:(loc_of_tacexpr br) env tbr ret in
+      let () = unify ?loc:(loc_of_tacexpr br) env tbr ret in
       intern_branch rem
     in
     let () = intern_branch pl in
@@ -971,7 +958,7 @@ and intern_case env loc e pl =
     | None ->
       let kn = match kn with Other kn -> kn | _ -> assert false in
       let cstr = pr_internal_constructor kn n is_const in
-      user_err ~loc (str "Unhandled match case for constructor " ++ cstr)
+      user_err ?loc (str "Unhandled match case for constructor " ++ cstr)
     | Some x -> x
     in
     let const = Array.mapi (fun i o -> map i true o) const in
@@ -980,11 +967,11 @@ and intern_case env loc e pl =
     (ce, ret)
   | PKind_open kn ->
     let subst, tc = fresh_reftype env (Other kn) in
-    let () = unify ~loc:(loc_of_tacexpr e) env t tc in
+    let () = unify ?loc:(loc_of_tacexpr e) env t tc in
     let ret = GTypVar (fresh_id env) in
     let rec intern_branch map = function
     | [] ->
-      user_err ~loc (str "Missing default case")
+      user_err ?loc (str "Missing default case")
     | (pat, br) :: rem ->
       match intern_patexpr env pat with
       | GPatVar na ->
@@ -997,23 +984,23 @@ and intern_case env loc e pl =
         let get = function
         | GPatVar na -> na
         | GPatRef _ ->
-          user_err ~loc (str "TODO: Unhandled match case") (** FIXME *)
+          user_err ?loc (str "TODO: Unhandled match case") (** FIXME *)
         in
         let loc = loc_of_patexpr pat in
         let knc = match knc with
         | Other knc -> knc
-        | Tuple n -> invalid_pattern ~loc (Other kn) (Tuple n)
+        | Tuple n -> invalid_pattern ?loc (Other kn) (Tuple n)
         in
         let ids = List.map get args in
         let data = Tac2env.interp_constructor knc in
         let () =
           if not (KerName.equal kn data.cdata_type) then
-            invalid_pattern ~loc (Other kn) (Other data.cdata_type)
+            invalid_pattern ?loc (Other kn) (Other data.cdata_type)
         in
         let nids = List.length ids in
         let nargs = List.length data.cdata_args in
         let () =
-          if not (Int.equal nids nargs) then error_nargs_mismatch loc knc nargs nids
+          if not (Int.equal nids nargs) then error_nargs_mismatch ?loc knc nargs nids
         in
         let fold env id tpe =
           (** Instantiate all arguments *)
@@ -1025,7 +1012,7 @@ and intern_case env loc e pl =
         let br' = intern_rec_with_constraint nenv br ret in
         let map =
           if KNmap.mem knc map then
-            let () = warn_redundant_clause ~loc () in
+            let () = warn_redundant_clause ?loc () in
             map
           else
             KNmap.add knc (Anonymous, Array.of_list ids, br') map
@@ -1053,7 +1040,7 @@ and intern_constructor env loc kn args = match kn with
     | None ->
       (GTacOpn (kn, args), ans)
   else
-    error_nargs_mismatch loc kn nargs (List.length args)
+    error_nargs_mismatch ?loc kn nargs (List.length args)
 | Tuple n ->
   assert (Int.equal n (List.length args));
   let types = List.init n (fun i -> GTypVar (fresh_id env)) in
@@ -1073,7 +1060,7 @@ and intern_record env loc fs =
   in
   let fs = List.map map fs in
   let kn = match fs with
-  | [] -> user_err ~loc (str "Cannot infer the corresponding record type")
+  | [] -> user_err ?loc (str "Cannot infer the corresponding record type")
   | (_, proj, _) :: _ -> proj.pdata_type
   in
   let params, typdef = match Tac2env.interp_type kn with
@@ -1104,7 +1091,7 @@ and intern_record env loc fs =
   | None -> ()
   | Some i ->
     let (field, _, _) = List.nth typdef i in
-    user_err ~loc (str "Field " ++ Id.print field ++ str " is undefined")
+    user_err ?loc (str "Field " ++ Id.print field ++ str " is undefined")
   in
   let args = Array.map_to_list Option.get args in
   let tparam = List.init params (fun i -> GTypVar subst.(i)) in
@@ -1204,18 +1191,18 @@ let get_projection0 var = match var with
   kn
 | AbsKn kn -> kn
 
-let rec globalize ids e = match e with
+let rec globalize ids (loc, er as e) = match er with
 | CTacAtm _ -> e
 | CTacRef ref ->
   let mem id = Id.Set.mem id ids in
   begin match get_variable0 mem ref with
   | ArgVar _ -> e
-  | ArgArg kn -> CTacRef (AbsKn kn)
+  | ArgArg kn -> Loc.tag ?loc @@ CTacRef (AbsKn kn)
   end
-| CTacCst (loc, qid) ->
+| CTacCst qid ->
   let knc = get_constructor () qid in
-  CTacCst (loc, AbsKn knc)
-| CTacFun (loc, bnd, e) ->
+  Loc.tag ?loc @@ CTacCst (AbsKn knc)
+| CTacFun (bnd, e) ->
   let fold (pats, accu) (pat, t) =
     let accu = ids_of_pattern accu pat in
     let pat = globalize_pattern ids pat in
@@ -1224,12 +1211,12 @@ let rec globalize ids e = match e with
   let bnd, ids = List.fold_left fold ([], ids) bnd in
   let bnd = List.rev bnd in
   let e = globalize ids e in
-  CTacFun (loc, bnd, e)
-| CTacApp (loc, e, el) ->
+  Loc.tag ?loc @@ CTacFun (bnd, e)
+| CTacApp (e, el) ->
   let e = globalize ids e in
   let el = List.map (fun e -> globalize ids e) el in
-  CTacApp (loc, e, el)
-| CTacLet (loc, isrec, bnd, e) ->
+  Loc.tag ?loc @@ CTacApp (e, el)
+| CTacLet (isrec, bnd, e) ->
   let fold accu (pat, _, _) = ids_of_pattern accu pat in
   let ext = List.fold_left fold Id.Set.empty bnd in
   let eids = Id.Set.union ext ids in
@@ -1239,48 +1226,48 @@ let rec globalize ids e = match e with
     (qid, t, globalize ids e)
   in
   let bnd = List.map map bnd in
-  CTacLet (loc, isrec, bnd, e)
-| CTacCnv (loc, e, t) ->
+  Loc.tag ?loc @@ CTacLet (isrec, bnd, e)
+| CTacCnv (e, t) ->
   let e = globalize ids e in
-  CTacCnv (loc, e, t)
-| CTacSeq (loc, e1, e2) ->
+  Loc.tag ?loc @@ CTacCnv (e, t)
+| CTacSeq (e1, e2) ->
   let e1 = globalize ids e1 in
   let e2 = globalize ids e2 in
-  CTacSeq (loc, e1, e2)
-| CTacCse (loc, e, bl) ->
+  Loc.tag ?loc @@ CTacSeq (e1, e2)
+| CTacCse (e, bl) ->
   let e = globalize ids e in
   let bl = List.map (fun b -> globalize_case ids b) bl in
-  CTacCse (loc, e, bl)
-| CTacRec (loc, r) ->
+  Loc.tag ?loc @@ CTacCse (e, bl)
+| CTacRec r ->
   let map (p, e) =
     let p = get_projection0 p in
     let e = globalize ids e in
     (AbsKn p, e)
   in
-  CTacRec (loc, List.map map r)
-| CTacPrj (loc, e, p) ->
+  Loc.tag ?loc @@ CTacRec (List.map map r)
+| CTacPrj (e, p) ->
   let e = globalize ids e in
   let p = get_projection0 p in
-  CTacPrj (loc, e, AbsKn p)
-| CTacSet (loc, e, p, e') ->
+  Loc.tag ?loc @@ CTacPrj (e, AbsKn p)
+| CTacSet (e, p, e') ->
   let e = globalize ids e in
   let p = get_projection0 p in
   let e' = globalize ids e' in
-  CTacSet (loc, e, AbsKn p, e')
-| CTacExt (loc, tag, arg) ->
+  Loc.tag ?loc @@ CTacSet (e, AbsKn p, e')
+| CTacExt (tag, arg) ->
   let arg = str (Tac2dyn.Arg.repr tag) in
-  CErrors.user_err ~loc (str "Cannot globalize generic arguments of type" ++ spc () ++ arg)
+  CErrors.user_err ?loc (str "Cannot globalize generic arguments of type" ++ spc () ++ arg)
 
 and globalize_case ids (p, e) =
   (globalize_pattern ids p, globalize ids e)
 
-and globalize_pattern ids p = match p with
+and globalize_pattern ids (loc, pr as p) = match pr with
 | CPatVar _ -> p
-| CPatRef (loc, cst, pl) ->
+| CPatRef (cst, pl) ->
   let knc = get_constructor () cst in
   let cst = AbsKn knc in
   let pl = List.map (fun p -> globalize_pattern ids p) pl in
-  CPatRef (loc, cst, pl)
+  Loc.tag ?loc @@ CPatRef (cst, pl)
 
 (** Kernel substitution *)
 
@@ -1387,16 +1374,16 @@ let subst_or_relid subst ref = match ref with
   let kn' = subst_or_tuple subst_kn subst kn in
   if kn' == kn then ref else AbsKn kn'
 
-let rec subst_rawtype subst t = match t with
+let rec subst_rawtype subst (loc, tr as t) = match tr with
 | CTypVar _ -> t
-| CTypArrow (loc, t1, t2) ->
+| CTypArrow (t1, t2) ->
   let t1' = subst_rawtype subst t1 in
   let t2' = subst_rawtype subst t2 in
-  if t1' == t1 && t2' == t2 then t else CTypArrow (loc, t1', t2')
-| CTypRef (loc, ref, tl) ->
+  if t1' == t1 && t2' == t2 then t else Loc.tag ?loc @@ CTypArrow (t1', t2')
+| CTypRef (ref, tl) ->
   let ref' = subst_or_relid subst ref in
   let tl' = List.smartmap (fun t -> subst_rawtype subst t) tl in
-  if ref' == ref && tl' == tl then t else CTypRef (loc, ref', tl')
+  if ref' == ref && tl' == tl then t else Loc.tag ?loc @@ CTypRef (ref', tl')
 
 let subst_tacref subst ref = match ref with
 | RelId _ -> ref
@@ -1413,35 +1400,35 @@ let subst_projection subst prj = match prj with
   let kn' = subst_kn subst kn in
   if kn' == kn then prj else AbsKn kn'
 
-let rec subst_rawpattern subst p = match p with
+let rec subst_rawpattern subst (loc, pr as p) = match pr with
 | CPatVar _ -> p
-| CPatRef (loc, c, pl) ->
+| CPatRef (c, pl) ->
   let pl' = List.smartmap (fun p -> subst_rawpattern subst p) pl in
   let c' = subst_or_relid subst c in
-  if pl' == pl && c' == c then p else CPatRef (loc, c', pl')
+  if pl' == pl && c' == c then p else Loc.tag ?loc @@ CPatRef (c', pl')
 
 (** Used for notations *)
-let rec subst_rawexpr subst t = match t with
+let rec subst_rawexpr subst (loc, tr as t) = match tr with
 | CTacAtm _ -> t
 | CTacRef ref ->
   let ref' = subst_tacref subst ref in
-  if ref' == ref then t else CTacRef ref'
-| CTacCst (loc, ref) ->
+  if ref' == ref then t else Loc.tag ?loc @@ CTacRef ref'
+| CTacCst ref ->
   let ref' = subst_or_relid subst ref in
-  if ref' == ref then t else CTacCst (loc, ref')
-| CTacFun (loc, bnd, e) ->
+  if ref' == ref then t else Loc.tag ?loc @@ CTacCst ref'
+| CTacFun (bnd, e) ->
   let map (na, t as p) =
     let t' = Option.smartmap (fun t -> subst_rawtype subst t) t in
     if t' == t then p else (na, t')
   in
   let bnd' = List.smartmap map bnd in
   let e' = subst_rawexpr subst e in
-  if bnd' == bnd && e' == e then t else CTacFun (loc, bnd', e')
-| CTacApp (loc, e, el) ->
+  if bnd' == bnd && e' == e then t else Loc.tag ?loc @@ CTacFun (bnd', e')
+| CTacApp (e, el) ->
   let e' = subst_rawexpr subst e in
   let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
-  if e' == e && el' == el then t else CTacApp (loc, e', el')
-| CTacLet (loc, isrec, bnd, e) ->
+  if e' == e && el' == el then t else Loc.tag ?loc @@ CTacApp (e', el')
+| CTacLet (isrec, bnd, e) ->
   let map (na, t, e as p) =
     let t' = Option.smartmap (fun t -> subst_rawtype subst t) t in
     let e' = subst_rawexpr subst e in
@@ -1449,16 +1436,16 @@ let rec subst_rawexpr subst t = match t with
   in
   let bnd' = List.smartmap map bnd in
   let e' = subst_rawexpr subst e in
-  if bnd' == bnd && e' == e then t else CTacLet (loc, isrec, bnd', e')
-| CTacCnv (loc, e, c) ->
+  if bnd' == bnd && e' == e then t else Loc.tag ?loc @@ CTacLet (isrec, bnd', e')
+| CTacCnv (e, c) ->
   let e' = subst_rawexpr subst e in
   let c' = subst_rawtype subst c in
-  if c' == c && e' == e then t else CTacCnv (loc, e', c')
-| CTacSeq (loc, e1, e2) ->
+  if c' == c && e' == e then t else Loc.tag ?loc @@ CTacCnv (e', c')
+| CTacSeq (e1, e2) ->
   let e1' = subst_rawexpr subst e1 in
   let e2' = subst_rawexpr subst e2 in
-  if e1' == e1 && e2' == e2 then t else CTacSeq (loc, e1', e2')
-| CTacCse (loc, e, bl) ->
+  if e1' == e1 && e2' == e2 then t else Loc.tag ?loc @@ CTacSeq (e1', e2')
+| CTacCse (e, bl) ->
   let map (p, e as x) =
     let p' = subst_rawpattern subst p in
     let e' = subst_rawexpr subst e in
@@ -1466,25 +1453,25 @@ let rec subst_rawexpr subst t = match t with
   in
   let e' = subst_rawexpr subst e in
   let bl' = List.smartmap map bl in
-  if e' == e && bl' == bl then t else CTacCse (loc, e', bl')
-| CTacRec (loc, el) ->
+  if e' == e && bl' == bl then t else Loc.tag ?loc @@ CTacCse (e', bl')
+| CTacRec el ->
   let map (prj, e as p) =
     let prj' = subst_projection subst prj in
     let e' = subst_rawexpr subst e in
     if prj' == prj && e' == e then p else (prj', e')
   in
   let el' = List.smartmap map el in
-  if el' == el then t else CTacRec (loc, el')
-| CTacPrj (loc, e, prj) ->
+  if el' == el then t else Loc.tag ?loc @@ CTacRec el'
+| CTacPrj (e, prj) ->
     let prj' = subst_projection subst prj in
     let e' = subst_rawexpr subst e in
-    if prj' == prj && e' == e then t else CTacPrj (loc, e', prj')
-| CTacSet (loc, e, prj, r) ->
+    if prj' == prj && e' == e then t else Loc.tag ?loc @@ CTacPrj (e', prj')
+| CTacSet (e, prj, r) ->
     let prj' = subst_projection subst prj in
     let e' = subst_rawexpr subst e in
     let r' = subst_rawexpr subst r in
-    if prj' == prj && e' == e && r' == r then t else CTacSet (loc, e', prj', r')
-| CTacExt _ -> assert false (** Should not be generated by gloabalization *)
+    if prj' == prj && e' == e && r' == r then t else Loc.tag ?loc @@ CTacSet (e', prj', r')
+| CTacExt _ -> assert false (** Should not be generated by globalization *)
 
 (** Registering *)
 
diff --git a/src/tac2intern.mli b/src/tac2intern.mli
index 95199d449d..045e657460 100644
--- a/src/tac2intern.mli
+++ b/src/tac2intern.mli
@@ -10,8 +10,8 @@ open Names
 open Mod_subst
 open Tac2expr
 
-val loc_of_tacexpr : raw_tacexpr -> Loc.t
-val loc_of_patexpr : raw_patexpr -> Loc.t
+val loc_of_tacexpr : raw_tacexpr -> Loc.t option
+val loc_of_patexpr : raw_patexpr -> Loc.t option
 
 val intern : raw_tacexpr -> glb_tacexpr * type_scheme
 val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quant_typedef
@@ -41,8 +41,8 @@ val globalize : Id.Set.t -> raw_tacexpr -> raw_tacexpr
 
 (** Errors *)
 
-val error_nargs_mismatch : Loc.t -> ltac_constructor -> int -> int -> 'a
-val error_nparams_mismatch : Loc.t -> int -> int -> 'a
+val error_nargs_mismatch : ?loc:Loc.t -> ltac_constructor -> int -> int -> 'a
+val error_nparams_mismatch : ?loc:Loc.t -> int -> int -> 'a
 
 (** Misc *)
 
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 279ab53b67..063a52c738 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -25,10 +25,9 @@ let control_core n = kername control_prefix n
 let dummy_loc = Loc.make_loc (-1, -1)
 
 let constructor ?loc kn args =
-  let loc = Option.default dummy_loc loc in
-  let cst = CTacCst (loc, AbsKn (Other kn)) in
+  let cst = Loc.tag ?loc @@ CTacCst (AbsKn (Other kn)) in
   if List.is_empty args then cst
-  else CTacApp (loc, cst, args)
+  else Loc.tag ?loc @@ CTacApp (cst, args)
 
 let std_constructor ?loc name args =
   constructor ?loc (std_core name) args
@@ -39,39 +38,35 @@ let std_proj ?loc name =
 let thunk e =
   let t_unit = coq_core "unit" in
   let loc = Tac2intern.loc_of_tacexpr e in
-  let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn (Other t_unit), []))] in
-  CTacFun (loc, var, e)
+  let var = [Loc.tag ?loc @@ CPatVar (Anonymous), Some (Loc.tag ?loc @@ CTypRef (AbsKn (Other t_unit), []))] in
+  Loc.tag ?loc @@ CTacFun (var, e)
 
 let of_pair f g (loc, (e1, e2)) =
-  let loc = Option.default dummy_loc loc in
-  CTacApp (loc, CTacCst (loc, AbsKn (Tuple 2)), [f e1; g e2])
+  Loc.tag ?loc @@ CTacApp (Loc.tag ?loc @@ CTacCst (AbsKn (Tuple 2)), [f e1; g e2])
 
 let of_tuple ?loc el = match el with
 | [] ->
-  let loc = Option.default dummy_loc loc in
-  CTacCst (loc, AbsKn (Tuple 0))
+  Loc.tag ?loc @@ CTacCst (AbsKn (Tuple 0))
 | [e] -> e
 | el ->
-  let loc = Option.default dummy_loc loc in
   let len = List.length el in
-  CTacApp (loc, CTacCst (loc, AbsKn (Tuple len)), el)
+  Loc.tag ?loc @@ CTacApp (Loc.tag ?loc @@ CTacCst (AbsKn (Tuple len)), el)
 
 let of_int (loc, n) =
-  CTacAtm (Loc.tag ?loc (AtmInt n))
+  Loc.tag ?loc @@ CTacAtm (AtmInt n)
 
 let of_option ?loc f opt = match opt with
 | None -> constructor ?loc (coq_core "None") []
 | Some e -> constructor ?loc (coq_core "Some") [f e]
 
 let inj_wit ?loc wit x =
-  let loc = Option.default dummy_loc loc in
-  CTacExt (loc, wit, x)
+  Loc.tag ?loc @@ CTacExt (wit, x)
 
 let of_variable (loc, id) =
   let qid = Libnames.qualid_of_ident id in
   if Tac2env.is_constructor qid then
     CErrors.user_err ?loc (str "Invalid identifier")
-  else CTacRef (RelId (Loc.tag ?loc qid))
+  else Loc.tag ?loc @@ CTacRef (RelId (Loc.tag ?loc qid))
 
 let of_anti f = function
 | QExpr x -> f x
@@ -171,10 +166,9 @@ let of_hyp_location ?loc ((occs, id), flag) =
   ]
 
 let of_clause (loc, cl) =
-  let loc = Option.default dummy_loc loc in
-  let hyps = of_option ~loc (fun l -> of_list ~loc of_hyp_location l) cl.q_onhyps in
+  let hyps = of_option ?loc (fun l -> of_list ?loc of_hyp_location l) cl.q_onhyps in
   let concl = of_occurrences cl.q_concl_occs in
-  CTacRec (loc, [
+  Loc.tag ?loc @@ CTacRec ([
     std_proj "on_hyps", hyps;
     std_proj "on_concl", concl;
   ])
@@ -191,8 +185,7 @@ let of_induction_clause (loc, cl) =
   let eqn = of_option ?loc of_intro_pattern_naming cl.indcl_eqn in
   let as_ = of_option ?loc of_or_and_intro_pattern cl.indcl_as in
   let in_ = of_option ?loc of_clause cl.indcl_in in
-  let loc = Option.default dummy_loc loc in
-  CTacRec (loc, [
+  Loc.tag ?loc @@ CTacRec ([
     std_proj "indcl_arg", arg;
     std_proj "indcl_eqn", eqn;
     std_proj "indcl_as", as_;
@@ -216,36 +209,32 @@ let of_rewriting (loc, rew) =
   in
   let repeat = of_repeat rew.rew_repeat in
   let equatn = thunk (of_constr_with_bindings rew.rew_equatn) in
-  let loc = Option.default dummy_loc loc in
-  CTacRec (loc, [
+  Loc.tag ?loc @@ CTacRec ([
     std_proj "rew_orient", orient;
     std_proj "rew_repeat", repeat;
     std_proj "rew_equatn", equatn;
   ])
 
 let of_hyp ?loc id =
-  let loc = Option.default dummy_loc loc in
-  let hyp = CTacRef (AbsKn (TacConstant (control_core "hyp"))) in
-  CTacApp (loc, hyp, [of_ident id])
+  let hyp = Loc.tag ?loc @@ CTacRef (AbsKn (TacConstant (control_core "hyp"))) in
+  Loc.tag ?loc @@ CTacApp (hyp, [of_ident id])
 
 let of_exact_hyp ?loc id =
-  let loc = Option.default dummy_loc loc in
-  let refine = CTacRef (AbsKn (TacConstant (control_core "refine"))) in
-  CTacApp (loc, refine, [thunk (of_hyp ~loc id)])
+  let refine = Loc.tag ?loc @@ CTacRef (AbsKn (TacConstant (control_core "refine"))) in
+  Loc.tag ?loc @@ CTacApp (refine, [thunk (of_hyp ?loc id)])
 
 let of_exact_var ?loc id =
-  let loc = Option.default dummy_loc loc in
-  let refine = CTacRef (AbsKn (TacConstant (control_core "refine"))) in
-  CTacApp (loc, refine, [thunk (of_variable id)])
+  let refine = Loc.tag ?loc @@ CTacRef (AbsKn (TacConstant (control_core "refine"))) in
+  Loc.tag ?loc @@ CTacApp (refine, [thunk (of_variable id)])
 
 let of_dispatch tacs =
-  let loc = Option.default dummy_loc (fst tacs) in
+  let (loc, _) = tacs in
   let default = function
   | Some e -> thunk e
-  | None -> thunk (CTacCst (loc, AbsKn (Tuple 0)))
+  | None -> thunk (Loc.tag ?loc @@ CTacCst (AbsKn (Tuple 0)))
   in
-  let map e = of_pair default (fun l -> of_list ~loc default l) (Loc.tag ~loc e) in
-  of_pair (fun l -> of_list ~loc default l) (fun r -> of_option ~loc map r) tacs
+  let map e = of_pair default (fun l -> of_list ?loc default l) (Loc.tag ?loc e) in
+  of_pair (fun l -> of_list ?loc default l) (fun r -> of_option ?loc map r) tacs
 
 let make_red_flag l =
   let open Genredexpr in
@@ -287,14 +276,13 @@ let of_reference r =
 
 let of_strategy_flag (loc, flag) =
   let open Genredexpr in
-  let loc = Option.default dummy_loc loc in
   let flag = make_red_flag flag in
-  CTacRec (loc, [
-    std_proj "rBeta", of_bool ~loc flag.rBeta;
-    std_proj "rMatch", of_bool ~loc flag.rMatch;
-    std_proj "rFix", of_bool ~loc flag.rFix;
-    std_proj "rCofix", of_bool ~loc flag.rCofix;
-    std_proj "rZeta", of_bool ~loc flag.rZeta;
-    std_proj "rDelta", of_bool ~loc flag.rDelta;
-    std_proj "rConst", of_list ~loc of_reference flag.rConst;
+  Loc.tag ?loc @@ CTacRec ([
+    std_proj "rBeta", of_bool ?loc flag.rBeta;
+    std_proj "rMatch", of_bool ?loc flag.rMatch;
+    std_proj "rFix", of_bool ?loc flag.rFix;
+    std_proj "rCofix", of_bool ?loc flag.rCofix;
+    std_proj "rZeta", of_bool ?loc flag.rZeta;
+    std_proj "rDelta", of_bool ?loc flag.rDelta;
+    std_proj "rConst", of_list ?loc of_reference flag.rConst;
   ])