[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.

6 files changed, 9 insertions, 9 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 0e94721589..2142cee374 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -802,7 +802,7 @@ let make_evar_universe_context e l =
   | None -> uctx
   | Some us ->
       List.fold_left
-        (fun uctx (loc,id) ->
+        (fun uctx { CAst.loc; v = id } ->
         fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx))
         uctx us
 
diff --git a/engine/evd.mli b/engine/evd.mli
index b28ce2a62d..84fa70ef2f 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -506,7 +506,7 @@ val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
 val evar_universe_context_of_binders :
   Universes.universe_binders -> UState.t
 
-val make_evar_universe_context : env -> (Id.t located) list option -> UState.t
+val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t
 val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t
diff --git a/engine/uState.ml b/engine/uState.ml
index 4b650c9c94..625495866e 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -282,7 +282,7 @@ let pr_uctx_level uctx l =
   Libnames.pr_reference (reference_of_level uctx l)
 
 type universe_decl =
-  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
 
 let error_unbound_universes left uctx =
   let open Univ in
@@ -305,7 +305,7 @@ let universe_context ~names ~extensible uctx =
   let levels = ContextSet.levels uctx.uctx_local in
   let newinst, left =
     List.fold_right
-      (fun (loc,id) (newinst, acc) ->
+      (fun { CAst.loc; v = id } (newinst, acc) ->
          let l =
            try UNameMap.find id (fst uctx.uctx_names)
            with Not_found -> assert false
@@ -325,7 +325,7 @@ let check_universe_context_set ~names ~extensible uctx =
   if extensible then ()
   else
     let open Univ in
-    let left = List.fold_left (fun left (loc,id) ->
+    let left = List.fold_left (fun left { CAst.loc; v = id } ->
         let l =
           try UNameMap.find id (fst uctx.uctx_names)
           with Not_found -> assert false
diff --git a/engine/uState.mli b/engine/uState.mli
index 6657d6047d..5c85b2b848 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -132,7 +132,7 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 val normalize : t -> t
 
 type universe_decl =
-  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
 
 (** [check_univ_decl ctx decl]
 
diff --git a/engine/universes.ml b/engine/universes.ml
index 3a00f0fd1d..f3660a5592 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -92,14 +92,14 @@ let register_universe_binders ref ubinders =
   if not (Id.Map.is_empty ubinders)
   then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
 
-type univ_name_list = Name.t Loc.located list
+type univ_name_list = Misctypes.lname list
 
 let universe_binders_with_opt_names ref levels = function
   | None -> universe_binders_of_global ref
   | Some udecl ->
     if Int.equal(List.length levels) (List.length udecl)
     then
-      List.fold_left2 (fun acc (_,na) lvl -> match na with
+      List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
           | Anonymous -> acc
           | Name na -> Names.Id.Map.add na lvl acc)
         empty_binders udecl levels
diff --git a/engine/universes.mli b/engine/universes.mli
index cb6e2ba1b6..04586a6f85 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -35,7 +35,7 @@ val empty_binders : universe_binders
 val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
 val universe_binders_of_global : Globnames.global_reference -> universe_binders
 
-type univ_name_list = Name.t Loc.located list
+type univ_name_list = Misctypes.lname list
 
 (** [universe_binders_with_opt_names ref u l]