[ast] Improve precision of Ast location recognition in serialization.

We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.

With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.

7 files changed, 62 insertions, 57 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 873505940..3c7095505 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -10,6 +10,7 @@
 open CErrors
 open Util
 open Pp
+open CAst
 open Names
 open Nameops
 open Libnames
@@ -151,7 +152,7 @@ let tag_var = tag Tag.variable
     if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n)
     else mt()
 
-  let pr_with_comments ?loc pp = pr_located (fun x -> x) (Loc.tag ?loc pp)
+  let pr_with_comments ?loc pp = pr_located (fun x -> x) (loc, pp)
 
   let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c)
 
@@ -220,28 +221,28 @@ let tag_var = tag Tag.variable
   let pr_expl_args pr (a,expl) =
     match expl with
       | None -> pr (lapp,L) a
-      | Some (_,ExplByPos (n,_id)) ->
+      | Some {v=ExplByPos (n,_id)} ->
         anomaly (Pp.str "Explicitation by position not implemented.")
-      | Some (_,ExplByName id) ->
+      | Some {v=ExplByName id} ->
         str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
 
   let pr_opt_type_spc pr = function
     | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt ()
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
-  let pr_lident (loc,id) =
+  let pr_lident {loc; v=id} =
     match loc with
     | None     -> pr_id id
     | Some loc -> let (b,_) = Loc.unloc loc in
-                  pr_located pr_id @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id
+                  pr_located pr_id (Some (Loc.make_loc (b,b + String.length (Id.to_string id))), id)
 
   let pr_lname = function
-    | (loc,Name id) -> pr_lident (loc,id)
-    | lna -> pr_located Name.print lna
+    | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id)
+    | x -> pr_ast Name.print x
 
   let pr_or_var pr = function
     | ArgArg x -> pr x
-    | ArgVar (loc,s) -> pr_lident (loc,s)
+    | ArgVar id -> pr_lident id
 
   let pr_prim_token = function
     | Numeral (n,s) -> str (if s then n else "-"^n)
@@ -315,7 +316,7 @@ let tag_var = tag Tag.variable
 
   let pr_patt = pr_patt mt
 
-  let pr_eqn pr (loc,(pl,rhs)) =
+  let pr_eqn pr {loc;v=(pl,rhs)} =
     spc() ++ hov 4
       (pr_with_comments ?loc
          (str "| " ++
@@ -323,12 +324,12 @@ let tag_var = tag Tag.variable
                    ++ str " =>") ++
             pr_sep_com spc (pr ltop) rhs))
 
-  let begin_of_binder l_bi = 
+  let begin_of_binder l_bi =
     let b_loc l = fst (Option.cata Loc.unloc (0,0) l) in
     match l_bi with
-    | CLocalDef((loc,_),_,_) -> b_loc loc
-    | CLocalAssum((loc,_)::_,_,_) -> b_loc loc
-    | CLocalPattern(loc,(_,_)) -> b_loc loc
+    | CLocalDef({loc},_,_) -> b_loc loc
+    | CLocalAssum({loc}::_,_,_) -> b_loc loc
+    | CLocalPattern{loc} -> b_loc loc
     | _ -> assert false
 
   let begin_of_binders = function
@@ -350,12 +351,12 @@ let tag_var = tag Tag.variable
       | Generalized (b, b', t') ->
         assert (match b with Implicit -> true | _ -> false);
         begin match nal with
-          |[loc,Anonymous] ->
+          |[{loc; v=Anonymous}] ->
             hov 1 (str"`" ++ (surround_impl b'
                                 ((if t' then str "!" else mt ()) ++ pr t)))
-          |[loc,Name id] ->
+          |[{loc; v=Name id}] ->
             hov 1 (str "`" ++ (surround_impl b'
-                                 (pr_lident (loc,id) ++ str " : " ++
+                                 (pr_lident CAst.(make ?loc id) ++ str " : " ++
                                     (if t' then str "!" else mt()) ++ pr t)))
           |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.")
         end
@@ -375,7 +376,7 @@ let tag_var = tag Tag.variable
       surround (pr_lname na ++
                 pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++
                 str" :=" ++ spc() ++ pr_c c)
-    | CLocalPattern (loc,(p,tyo)) ->
+    | CLocalPattern {CAst.loc; v = p,tyo} ->
       let p = pr_patt lsimplepatt p in
       match tyo with
         | None ->
@@ -410,7 +411,7 @@ let tag_var = tag Tag.variable
   let pr_guard_annot pr_aux bl (n,ro) =
     match n with
       | None -> mt ()
-      | Some (loc, id) ->
+      | Some {loc; v = id} ->
         match (ro : Constrexpr.recursion_order_expr) with
           | CStructRec ->
             let names_of_binder = function
@@ -427,11 +428,11 @@ let tag_var = tag Tag.variable
             spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++
               (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}"
 
-  let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) =
+  let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) =
     let annot = pr_guard_annot (pr lsimpleconstr) bl ro in
     pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
-  let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) =
+  let pr_cofixdecl pr prd dangling_with_for ({v=id},bl,t,c) =
     pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
 
   let pr_recursive pr_decl id = function
@@ -461,7 +462,7 @@ let tag_var = tag Tag.variable
 
   let pr_simple_return_type pr na po =
     (match na with
-      | Some (_,Name id) ->
+      | Some {v=Name id} ->
         spc () ++ keyword "as" ++ spc () ++ pr_id id
       | _ -> mt ()) ++
       pr_case_type pr po
@@ -492,7 +493,7 @@ let tag_var = tag Tag.variable
   let pr_fun_sep = spc () ++ str "=>"
 
   let pr_dangling_with_for sep pr inherited a =
-    match a.CAst.v with
+    match a.v with
       | (CFix (_,[_])|CCoFix(_,[_])) ->
         pr sep (latom,E) a
       | _ ->
@@ -507,14 +508,14 @@ let tag_var = tag Tag.variable
         return (
           hov 0 (keyword "fix" ++ spc () ++
                    pr_recursive
-                   (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix),
+                   (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v fix),
           lfix
         )
       | CCoFix (id,cofix) ->
         return (
           hov 0 (keyword "cofix" ++ spc () ++
                    pr_recursive
-                   (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix),
+                   (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v cofix),
           lfix
         )
       | CProdN (bl,a) ->
@@ -533,8 +534,8 @@ let tag_var = tag Tag.variable
               pr_fun_sep ++ pr spc ltop a),
           llambda
         )
-      | CLetIn ((_,Name x), ({ CAst.v = CFix((_,x'),[_])}
-                          |  { CAst.v = CCoFix((_,x'),[_]) } as fx), t, b)
+      | CLetIn ({v=Name x}, ({ v = CFix({v=x'},[_])}
+                          |  { v = CCoFix({v=x'},[_]) } as fx), t, b)
           when Id.equal x x' ->
         return (
           hv 0 (
@@ -590,7 +591,7 @@ let tag_var = tag Tag.variable
           hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
           latom
         )
-      | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([[p]],b))]) ->
+      | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) ->
         return (
           hv 0 (
             keyword "let" ++ spc () ++ str"'" ++
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 158906dd2..cedeed5f3 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -10,7 +10,6 @@
     objects and their subcomponents. *)
 
 (** The default pretty-printers produce pretty-printing commands ({!Pp.t}). *)
-open Loc
 open Libnames
 open Constrexpr
 open Names
@@ -23,8 +22,8 @@ val pr_tight_coma : unit -> Pp.t
 
 val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
 
-val pr_lident : Id.t located -> Pp.t
-val pr_lname : Name.t located -> Pp.t
+val pr_lident : lident -> Pp.t
+val pr_lname : lname -> Pp.t
 
 val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
 val pr_com_at : int -> Pp.t
@@ -44,7 +43,7 @@ val pr_glob_level : glob_level -> Pp.t
 val pr_glob_sort : glob_sort -> Pp.t
 val pr_guard_annot : (constr_expr -> Pp.t) ->
   local_binder_expr list ->
-  ('a * Names.Id.t) option * recursion_order_expr ->
+  lident option * recursion_order_expr ->
   Pp.t
 
 val pr_record_body : (reference * constr_expr) list -> Pp.t
diff --git a/printing/pputils.ml b/printing/pputils.ml
index a544b4762..e779fc5fc 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -24,9 +24,11 @@ let pr_located pr (loc, x) =
     before ++ x ++ after
   | _ -> pr x
 
+let pr_ast pr { CAst.loc; v } = pr_located pr (loc, v)
+
 let pr_or_var pr = function
   | ArgArg x -> pr x
-  | ArgVar (_,s) -> Names.Id.print s
+  | ArgVar {CAst.v=s} -> Names.Id.print s
 
 let pr_with_occurrences pr keyword (occs,c) =
   match occs with
diff --git a/printing/pputils.mli b/printing/pputils.mli
index f7f586b77..ec5c32fc4 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -12,6 +12,7 @@ open Locus
 open Genredexpr
 
 val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t
+val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t
 (** Prints an object surrounded by its commented location *)
 
 val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 31c0d20f3..83cac7ddd 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -11,6 +11,8 @@ open Names
 
 open CErrors
 open Util
+open CAst
+
 open Extend
 open Vernacexpr
 open Pputils
@@ -59,7 +61,7 @@ open Decl_kinds
 
   let pr_ident_decl (lid, l) =
     pr_lident lid ++ pr_universe_decl l
-    
+
   let string_of_fqid fqid =
     String.concat "." (List.map Id.to_string fqid)
 
@@ -236,7 +238,7 @@ open Decl_kinds
       keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
         pr_located pr_qualid qid
 
-  let rec pr_module_ast leading_space pr_c = let open CAst in function
+  let rec pr_module_ast leading_space pr_c = function
     | { loc ; v = CMident qid } ->
       if leading_space then
         spc () ++ pr_located pr_qualid (loc, qid)
@@ -287,10 +289,10 @@ open Decl_kinds
     prlist_strict (pr_module_vardecls pr_c) l
 
   let pr_type_option pr_c = function
-    | { CAst.v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt()
+    | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt()
     | _ as c -> brk(0,2) ++ str" :" ++ pr_c c
 
-  let pr_decl_notation prc ((loc,ntn),c,scopt) =
+  let pr_decl_notation prc ({loc; v=ntn},c,scopt) =
     fnl () ++ keyword "where " ++ qs ntn ++ str " := "
     ++ Flags.without_option Flags.beautify prc c ++
       pr_opt (fun sc -> str ": " ++ str sc) scopt
@@ -329,7 +331,7 @@ open Decl_kinds
 
   let begin_of_inductive = function
     | [] -> 0
-    | (_,((loc,_),_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc
+    | (_,({loc},_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc
 
   let pr_class_rawexpr = function
     | FunClass -> keyword "Funclass"
@@ -392,8 +394,8 @@ open Decl_kinds
     | SetOnlyPrinting -> keyword "only printing"
     | SetOnlyParsing -> keyword "only parsing"
     | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
-    | SetFormat("text",s) -> keyword "format " ++ pr_located qs s
-    | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s
+    | SetFormat("text",s) -> keyword "format " ++ pr_ast qs s
+    | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s
 
   let pr_syntax_modifiers = function
     | [] -> mt()
@@ -537,7 +539,7 @@ open Decl_kinds
     let rec aux = function
       | SsEmpty -> "()"
       | SsType -> "(Type)"
-      | SsSingl (_,id) -> "("^Id.to_string id^")"
+      | SsSingl { v=id } -> "("^Id.to_string id^")"
       | SsCompl e -> "-" ^ aux e^""
       | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
       | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
@@ -661,7 +663,7 @@ open Decl_kinds
           ++ spc() ++ pr_smart_global q
           ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
         )
-      | VernacInfix (((_,s),mv),q,sn) -> (* A Verifier *)
+      | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *)
         return (
           hov 0 (hov 0 (keyword "Infix "
                         ++ qs s ++ str " :=" ++ pr_constrarg q) ++
@@ -670,7 +672,7 @@ open Decl_kinds
                      | None -> mt()
                      | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
         )
-      | VernacNotation (c,((_,s),l),opt) ->
+      | VernacNotation (c,({v=s},l),opt) ->
         return (
           hov 2 (keyword "Notation" ++ spc() ++ qs s ++
                    str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
@@ -680,7 +682,7 @@ open Decl_kinds
         )
       | VernacSyntaxExtension (_, (s, l)) ->
         return (
-          keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++
+          keyword "Reserved Notation" ++ spc() ++ pr_ast qs s ++
             pr_syntax_modifiers l
         )
       | VernacNotationAddFormat(s,k,v) ->
@@ -692,7 +694,7 @@ open Decl_kinds
       | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
         let pr_def_token dk =
           keyword (
-            if Name.is_anonymous (snd (fst id))
+            if Name.is_anonymous (fst id).v
             then "Goal"
             else Kindops.string_of_definition_object_kind dk)
         in
@@ -711,7 +713,7 @@ open Decl_kinds
             in
             (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
           | ProveBody (bl,t) ->
-            let typ u = if snd (fst id) = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
+            let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
             (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in
         let (binds,typ,c) = pr_def_body b in
         return (
@@ -889,16 +891,16 @@ open Decl_kinds
         return (
           hov 1 (
             (if abst then keyword "Declare" ++ spc () else mt ()) ++
-              keyword "Instance" ++
-              (match instid with
-      	 | (loc, Name id), l -> spc () ++ pr_ident_decl ((loc, id),l) ++ spc ()
-               | (_, Anonymous), _ -> mt ()) ++
-              pr_and_type_binders_arg sup ++
+            keyword "Instance" ++
+            (match instid with
+             | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc ()
+             | { v = Anonymous }, _ -> mt ()) ++
+            pr_and_type_binders_arg sup ++
               str":" ++ spc () ++
               (match bk with Implicit -> str "! " | Explicit -> mt ()) ++
               pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++
               (match props with
-                | Some (true, { CAst.v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
+                | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
                 | Some (true,_) -> assert false
                 | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
                 | None -> mt()))
@@ -1031,7 +1033,7 @@ open Decl_kinds
           hov 2 (
             keyword "Arguments" ++ spc() ++
               pr_smart_global q ++
-              let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
+              let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in
               let pr_if b x = if b then x else str "" in
               let pr_br imp x = match imp with
                 | Vernacexpr.Implicit -> str "[" ++ x ++ str "]"
@@ -1237,9 +1239,9 @@ let pr_vernac_flag =
         (fun f a -> pr_vernac_flag f ++ spc() ++ a)
         f
         (pr_vernac_expr v' ++ sep_end v')
-    | VernacTime (_,(_,v)) ->
+    | VernacTime (_,{v}) ->
       return (keyword "Time" ++ spc() ++ pr_vernac_control v)
-    | VernacRedirect (s, (_,v)) ->
+    | VernacRedirect (s, {v}) ->
       return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
     | VernacTimeout(n,v) ->
       return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v)
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index fd7f1f92b..c1d8f1d37 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -33,10 +33,10 @@ val print_eval :
     Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
 val print_name : env -> Evd.evar_map -> reference or_by_notation ->
-  Vernacexpr.univ_name_list option -> Pp.t
+  Universes.univ_name_list option -> Pp.t
 val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
 val print_about : env -> Evd.evar_map -> reference or_by_notation ->
-  Vernacexpr.univ_name_list option -> Pp.t
+  Universes.univ_name_list option -> Pp.t
 val print_impargs : reference or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 97ed063fe..4f15dd393 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -13,6 +13,6 @@ val printable_body : DirPath.t -> bool
 
 val pr_mutual_inductive_body : Environ.env ->
   MutInd.t -> Declarations.mutual_inductive_body ->
-  Vernacexpr.univ_name_list option -> Pp.t
+  Universes.univ_name_list option -> Pp.t
 val print_module : bool -> ModPath.t -> Pp.t
 val print_modtype : ModPath.t -> Pp.t