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

1 files changed, 3 insertions, 3 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 57436784b..7661fff6d 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -214,7 +214,7 @@ let fresh_name_for_anonymous_theorem () =
   let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
   next_global_ident_away default_thm_id avoid
 
-let check_name_freshness locality (loc,id) : unit =
+let check_name_freshness locality {CAst.loc;v=id} : unit =
   (* We check existence here: it's a bit late at Qed time *)
   if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
      locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
@@ -339,7 +339,7 @@ let universe_proof_terminator compute_guard hook =
         (hook (Some (proof.Proof_global.universes))) is_opaque in
       begin match idopt with
       | None -> save_named ~export_seff proof
-      | Some (_,id) -> save_anonymous ~export_seff proof id
+      | Some { CAst.v = id } -> save_anonymous ~export_seff proof id
       end
   end
 
@@ -444,7 +444,7 @@ let start_proof_com ?inference_hook kind thms hook =
     let ids = List.map RelDecl.get_name ctx in
     check_name_freshness (pi1 kind) id;
     (* XXX: The nf_evar is critical !! *)
-    evd, (snd id,
+    evd, (id.CAst.v,
           (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
            (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
       evd thms in