[located] More work towards using CAst.t

We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:

- module declarations
- intro patterns
- top-level sentences

Now, parsed documents should be full annotated by `CAst` nodes.

3 files changed, 5 insertions, 5 deletions

diff --git a/printing/pputils.ml b/printing/pputils.ml
index 010b92f3e..c2846c4cd 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -124,7 +124,7 @@ let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
 
 let pr_or_by_notation f = function
   | AN v -> f v
-  | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+  | ByNotation {CAst.v=(s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
 let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index ea1ca26fb..5c5b7206a 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -69,7 +69,7 @@ open Decl_kinds
 
   let pr_fqid fqid = str (string_of_fqid fqid)
 
-  let pr_lfqid (loc,fqid) =
+  let pr_lfqid {CAst.loc;v=fqid} =
     match loc with
     | None     -> pr_fqid fqid
     | Some loc -> let (b,_) = Loc.unloc loc in
@@ -238,7 +238,7 @@ open Decl_kinds
       keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p
     | CWith_Module (id,qid) ->
       keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
-        pr_located pr_qualid qid
+        pr_ast pr_qualid qid
 
   let rec pr_module_ast leading_space pr_c = function
     | { loc ; v = CMident qid } ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 9da94e42a..cfc5e6b4e 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -838,7 +838,7 @@ let print_any_name env sigma na udecl =
 
 let print_name env sigma na udecl =
   match na with
-  | ByNotation (loc,(ntn,sc)) ->
+  | ByNotation {CAst.loc;v=(ntn,sc)} ->
       print_any_name env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc))
@@ -891,7 +891,7 @@ let print_about_any ?loc env sigma k udecl =
 
 let print_about env sigma na udecl =
   match na with
-  | ByNotation (loc,(ntn,sc)) ->
+  | ByNotation {CAst.loc;v=(ntn,sc)} ->
       print_about_any ?loc env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc)) udecl